1  /-
  2  Copyright (c) 2018 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau, Mario Carneiro, Johan Commelin
  5  -/
  6  import tactic.ring data.quot data.equiv.algebra ring_theory.ideal_operations group_theory.submonoid
src         └─────────┘ └───────┘ └────────────────┘ └──────────────────────────┘ └────────────────────┘
  7  
  8  universes u v
  9  
 10  namespace localization
 11  variables (α : Type u) [comm_ring α] (S : set α) [is_submonoid S]
 12  
 13  def r (x y : α × S) : Prop :=
 14  ∃ t ∈ S, ((x.2 : α) * y.1 - y.2 * x.1) * t = 0
 15  
 16  local infix ≈ := r α S
 17  
 18  section
 19  variables {α S}
 20  theorem r_of_eq {a₀ a₁ : α × S} (h : (a₀.2 : α) * a₁.1 = a₁.2 * a₀.1) : a₀ ≈ a₁ :=
 21  ⟨1, is_submonoid.one_mem S, by rw [h, sub_self, mul_one]⟩
id                                                         
src                                 └──┘ └┘        └┘      
typ                                 └──┘ └┘        └┘      
doc                                 └──┘ └┘        └┘       
txt                                 └──┘ └┘        └┘       
par                                 └──┘ └┘        └┘       
pid                                   └┘ └┘        └┘       
st                                                         
 22  end
 23  
 24  theorem refl (x : α × S) : x ≈ x := r_of_eq rfl
id                                 └─────┘ └─┘
src                                    └─────┘ └─┘
typ                                └─────┘ └─┘
 25  
 26  theorem symm (x y : α × S) : x ≈ y → y ≈ x :=
id                                    
src                                       
typ                                   
 27  λ ⟨t, hts, ht⟩, ⟨t, hts, by rw [← neg_sub, ← neg_mul_eq_neg_mul, ht, neg_zero]⟩
id       └─┘                         └─────┘    └────────────────┘  └┘  └──────┘
src                              └────┘└─────┘└──┘└────────────────┘└┘  └┘└──────┘
typ      └─┘                   └────┘└─────┘└──┘└────────────────┘└┘└┘└┘└──────┘
doc                              └────┘       └──┘                  └┘  └┘        
txt                              └────┘       └──┘                  └┘  └┘        
par                              └────┘       └──┘                  └┘  └┘        
pid                                └──┘       └──┘                  └┘  └┘        
st                              └────────────┘└────────────────────┘└──┘└────────┘
 28  
 29  theorem trans : ∀ (x y z : α × S), x ≈ y → y ≈ z → x ≈ z :=
id                                               
src                                                    
typ                                              
 30  λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨t, hts, ht⟩ ⟨t', hts', ht'⟩,
 31  ⟨s₂ * t' * t, is_submonoid.mul_mem (is_submonoid.mul_mem hs₂ hts') hts,
id                 └──────────────────┘  └──────────────────┘
src                └──────────────────┘  └──────────────────┘
typ                └──────────────────┘  └──────────────────┘
 32    calc (s₁ * r₃ - s₃ * r₁) * (s₂ * t' * t) =
 33      t' * s₃ * ((s₁ * r₂ - s₂ * r₁) * t) + t * s₁ * ((s₂ * r₃ - s₃ * r₂) * t') :
 34        by simp [mul_left_comm, mul_add, mul_comm]
src           └────┘             └┘       └┘        └─
typ           └────┘             └┘       └┘        └─
doc           └────┘             └┘       └┘        └─
txt           └────┘             └┘       └┘        └─
par           └────┘             └┘       └┘        └─
pid                            └┘       └┘        
 35      ... = 0 : by simp only [subtype.coe_mk] at ht ht'; rw [ht, ht']; simp⟩
id                                                                   └┘
src  ───┘             └─────────┘              └─────────┘  └──┘  └┘     └──┘
typ  ───┘             └─────────┘              └─────────┘  └──┘  └┘ └┘  └──┘
doc  ───┘             └─────────┘              └─────────┘  └──┘  └┘     └──┘
txt  ───┘             └─────────┘              └─────────┘  └──┘  └┘     └──┘
par  ───┘             └─────────┘              └─────────┘  └──┘  └┘     └──┘
pid  ───┘                 └──┘└┘              └───────┘    └┘  └┘   
st                                                                   └┘└────┘
 36  
 37  instance : setoid (α × S) :=
id              └────┘    
src             └────┘    
typ             └────┘    
 38  ⟨r α S, refl α S, symm α S, trans α S⟩
id        └──┘    └──┘    └───┘  
src         └──┘      └──┘      └───┘
typ       └──┘    └──┘    └───┘  
 39  
 40  end localization
 41  
 42  /-- The localization of a ring at a submonoid:
 43   the elements of the submonoid become invertible in the localization.-/
 44  def localization (α : Type u) [comm_ring α] (S : set α) [is_submonoid S] :=
id                                  └───────┘        └─┘    └──────────┘ 
src                                 └───────┘         └─┘     └──────────┘
typ                                 └───────┘        └─┘    └──────────┘ 
doc                                                           └──────────┘
 45  quotient $ localization.setoid α S
id   └──────┘   └─────────────────┘  
src  └──────┘   └─────────────────┘
typ  └──────┘   └─────────────────┘  
 46  
 47  namespace localization
 48  variables (α : Type u) [comm_ring α] (S : set α) [is_submonoid S]
id                           └───────┘         └─┘     └──────────┘
src                          └───────┘         └─┘     └──────────┘
typ                          └───────┘         └─┘     └──────────┘
doc                                                    └──────────┘
 49  
 50  instance : has_add (localization α S) :=
 51  ⟨quotient.lift₂
 52    (λ x y : α × S, (⟦⟨x.2 * y.1 + y.2 * x.1, x.2 * y.2⟩⟧ : localization α S)) $
 53    λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
 54    quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
 55      calc (s₁ * s₂ * (s₃ * r₄ + s₄ * r₃) - s₃ * s₄ * (s₁ * r₂ + s₂ * r₁)) * (t₆ * t₅) =
 56        s₁ * s₃ * ((s₂ * r₄ - s₄ * r₂) * t₆) * t₅ + s₂ * s₄ * ((s₁ * r₃ - s₃ * r₁) * t₅) * t₆ : by ring
src                                                                                                   └────
typ                                                                                                   └────
doc                                                                                                   └────
txt                                                                                                   └────
par                                                                                                   └────
pid                                                                                                       
 57        ... = 0 : by simp only [subtype.coe_mk] at ht₅ ht₆; rw [ht₆, ht₅]; simp⟩⟩
src  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
typ  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
doc  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
txt  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
par  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
pid  ─────┘                 └──┘└┘              └────────┘    └┘   └┘   
 58  
 59  instance : has_neg (localization α S) :=
 60  ⟨quotient.lift (λ x : α × S, (⟦⟨-x.1, x.2⟩⟧ : localization α S)) $
 61    λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨t, hts, ht⟩,
 62    quotient.sound ⟨t, hts,
 63      calc (s₁ * -r₂ - s₂ * -r₁) * t = -((s₁ * r₂ - s₂ * r₁) * t) : by ring
src                                                                       └────
typ                                                                       └────
doc                                                                       └────
txt                                                                       └────
par                                                                       └────
pid                                                                           
 64        ... = 0 : by simp only [subtype.coe_mk] at ht; rw ht; simp⟩⟩
src  ─────┘             └─────────┘              └─────┘  └─┘    └──┘
typ  ─────┘             └─────────┘              └─────┘  └─┘    └──┘
doc  ─────┘             └─────────┘              └─────┘  └─┘    └──┘
txt  ─────┘             └─────────┘              └─────┘  └─┘    └──┘
par  ─────┘             └─────────┘              └─────┘  └─┘    └──┘
pid  ─────┘                 └──┘└┘              └───┘    
 65  
 66  instance : has_mul (localization α S) :=
 67  ⟨quotient.lift₂
 68    (λ x y : α × S, (⟦⟨x.1 * y.1, x.2 * y.2⟩⟧ : localization α S)) $
 69    λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
 70    quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
 71      calc ((s₁ * s₂) * (r₃ * r₄) - (s₃ * s₄) * (r₁ * r₂)) * (t₆ * t₅) =
 72        t₆ * ((s₁ * r₃ - s₃ * r₁) * t₅) * r₂ * s₄ + t₅ * ((s₂ * r₄ - s₄ * r₂) * t₆) * r₃ * s₁ :
 73          by simp [mul_left_comm, mul_add, mul_comm]
src             └────┘             └┘       └┘        └─
typ             └────┘             └┘       └┘        └─
doc             └────┘             └┘       └┘        └─
txt             └────┘             └┘       └┘        └─
par             └────┘             └┘       └┘        └─
pid                              └┘       └┘        
 74        ... = 0 : by simp only [subtype.coe_mk] at ht₅ ht₆; rw [ht₅, ht₆]; simp⟩⟩
src  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
typ  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
doc  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
txt  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
par  ─────┘             └─────────┘              └──────────┘  └──┘   └┘     └──┘
pid  ─────┘                 └──┘└┘              └────────┘    └┘   └┘   
 75  
 76  variables {α S}
 77  
 78  def mk (r : α) (s : S) : localization α S := ⟦(r, s)⟧
id                          └──────────┘         
src                           └──────────┘             
typ                         └──────────┘         
doc                           └──────────┘
 79  
 80  /-- The natural map from the ring to the localization.-/
 81  def of (r : α) : localization α S := mk r 1
id                   └──────────┘      └┘ 
src                   └──────────┘        └┘
typ                  └──────────┘      └┘ 
doc                   └──────────┘
 82  
 83  instance : comm_ring (localization α S) :=
 84  by refine
src     └─────┘
typ     └─────┘
doc     └─────┘
txt     └─────┘
par     └─────┘
pid           
 85  { add            := has_add.add,
src   └─────────────────┘           └─
typ   └─────────────────┘           └─
doc   └─────────────────┘           └─
txt   └─────────────────┘           └─
par   └─────────────────┘           └─
pid   └─────────────────┘           └─
 86    add_assoc      := λ m n k, quotient.induction_on₃ m n k _,
src  ───────────────────┘ └──────┘                         └───
typ  ───────────────────┘ └──────┘                         └───
doc  ───────────────────┘ └──────┘                         └───
txt  ───────────────────┘ └──────┘                         └───
par  ───────────────────┘ └──────┘                         └───
pid  ───────────────────┘ └──────┘                         └───
 87    zero           := of 0,
src  ───────────────────┘  └───
typ  ───────────────────┘  └───
doc  ───────────────────┘  └───
txt  ───────────────────┘  └───
par  ───────────────────┘  └───
pid  ───────────────────┘  └───
 88    zero_add       := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
 89    add_zero       := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
 90    neg            := has_neg.neg,
src  ───────────────────┘           └─
typ  ───────────────────┘           └─
doc  ───────────────────┘           └─
txt  ───────────────────┘           └─
par  ───────────────────┘           └─
pid  ───────────────────┘           └─
 91    add_left_neg   := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
 92    add_comm       := quotient.ind₂ _,
src  ───────────────────┘             └───
typ  ───────────────────┘             └───
doc  ───────────────────┘             └───
txt  ───────────────────┘             └───
par  ───────────────────┘             └───
pid  ───────────────────┘             └───
 93    mul            := has_mul.mul,
src  ───────────────────┘           └─
typ  ───────────────────┘           └─
doc  ───────────────────┘           └─
txt  ───────────────────┘           └─
par  ───────────────────┘           └─
pid  ───────────────────┘           └─
 94    mul_assoc      := λ m n k, quotient.induction_on₃ m n k _,
src  ───────────────────┘ └──────┘                         └───
typ  ───────────────────┘ └──────┘                         └───
doc  ───────────────────┘ └──────┘                         └───
txt  ───────────────────┘ └──────┘                         └───
par  ───────────────────┘ └──────┘                         └───
pid  ───────────────────┘ └──────┘                         └───
 95    one            := of 1,
src  ───────────────────┘  └───
typ  ───────────────────┘  └───
doc  ───────────────────┘  └───
txt  ───────────────────┘  └───
par  ───────────────────┘  └───
pid  ───────────────────┘  └───
 96    one_mul        := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
 97    mul_one        := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
 98    left_distrib   := λ m n k, quotient.induction_on₃ m n k _,
src  ───────────────────┘ └──────┘                         └───
typ  ───────────────────┘ └──────┘                         └───
doc  ───────────────────┘ └──────┘                         └───
txt  ───────────────────┘ └──────┘                         └───
par  ───────────────────┘ └──────┘                         └───
pid  ───────────────────┘ └──────┘                         └───
 99    right_distrib  := λ m n k, quotient.induction_on₃ m n k _,
src  ───────────────────┘ └──────┘                         └───
typ  ───────────────────┘ └──────┘                         └───
doc  ───────────────────┘ └──────┘                         └───
txt  ───────────────────┘ └──────┘                         └───
par  ───────────────────┘ └──────┘                         └───
pid  ───────────────────┘ └──────┘                         └───
100    mul_comm       := quotient.ind₂ _ };
src  ───────────────────┘             └──┘
typ  ───────────────────┘             └──┘
doc  ───────────────────┘             └──┘
txt  ───────────────────┘             └──┘
par  ───────────────────┘             └──┘
pid  ───────────────────┘             └──┘
101  { intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
102    try {rcases a with ⟨r₁, s₁, hs₁⟩},
src    └───┘└─────┘ └─────────────────┘
typ    └───┘└─────┘ └─────────────────┘
doc    └───┘└─────┘ └─────────────────┘
txt    └───┘└─────┘ └─────────────────┘
par    └───┘└─────┘ └─────────────────┘
pid       └───────┘ └──────────────────┘
103    try {rcases b with ⟨r₂, s₂, hs₂⟩},
src    └───┘└─────┘ └─────────────────┘
typ    └───┘└─────┘ └─────────────────┘
doc    └───┘└─────┘ └─────────────────┘
txt    └───┘└─────┘ └─────────────────┘
par    └───┘└─────┘ └─────────────────┘
pid       └───────┘ └──────────────────┘
104    try {rcases c with ⟨r₃, s₃, hs₃⟩},
src    └───┘└─────┘ └─────────────────┘
typ    └───┘└─────┘ └─────────────────┘
doc    └───┘└─────┘ └─────────────────┘
txt    └───┘└─────┘ └─────────────────┘
par    └───┘└─────┘ └─────────────────┘
pid       └───────┘ └──────────────────┘
105    refine (quotient.sound $ r_of_eq _),
src    └─────┘                       └─┘
typ    └─────┘                       └─┘
doc    └─────┘                       └─┘
txt    └─────┘                       └─┘
par    └─────┘                       └─┘
pid                                 └─┘
106    simp [mul_left_comm, mul_add, mul_comm] }
src    └────┘             └┘       └┘        └┘
typ    └────┘             └┘       └┘        └┘
doc    └────┘             └┘       └┘        └┘
txt    └────┘             └┘       └┘        └┘
par    └────┘             └┘       └┘        └┘
pid                     └┘       └┘        
107  
108  instance : inhabited (localization α S) := ⟨0⟩
109  
110  instance of.is_ring_hom : is_ring_hom (of : α → localization α S) :=
111  { map_add := λ x y, quotient.sound $ by simp,
src                                          └──┘
typ                                          └──┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
112    map_mul := λ x y, quotient.sound $ by simp,
id                                 └──┘
src                                └──┘      └──┘
typ                                └──┘      └──┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
st                                          └───┘
113    map_one := rfl }
id                └─┘
src               └─┘
typ               └─┘
114  
115  variables {S}
116  
117  instance : has_coe_t α (localization α S) := ⟨of⟩ -- note [use has_coe_t]
id              └───────┘   └──────────┘        └┘
src             └───────┘    └──────────┘          └┘
typ             └───────┘   └──────────┘        └┘
doc             └───────┘    └──────────┘          └┘
118  
119  instance coe.is_ring_hom : is_ring_hom (coe : α → localization α S) :=
id                              └─────────┘  └─┘      └──────────┘  
src                             └─────────┘  └─┘       └──────────┘
typ                             └─────────┘  └─┘      └──────────┘  
doc                             └─────────┘            └──────────┘
120  localization.of.is_ring_hom
id   └─────────────────────────┘
src  └─────────────────────────┘
typ  └─────────────────────────┘
121  
122  /-- The natural map from the submonoid to the unit group of the localization.-/
123  def to_units (s : S) : units (localization α S) :=
id                         └───┘  └──────────┘  
src                         └───┘  └──────────┘
typ                        └───┘  └──────────┘  
doc                                └──────────┘
124  { val := s,
id            
typ           
125    inv := mk 1 s,
id            └┘   
src           └┘
typ           └┘   
126    val_inv := quotient.sound $ r_of_eq $ mul_assoc _ _ _,
id                └────────────┘   └─────┘   └───────┘
src               └────────────┘   └─────┘   └───────┘
typ               └────────────┘   └─────┘   └───────┘
127    inv_val := quotient.sound $ r_of_eq $ show s.val * 1 * 1 = 1 * (1 * s.val), by simp }
id                └────────────┘   └─────┘        └──┘               └──┘
src               └────────────┘   └─────┘         └──┘                └──┘      └───┘
typ               └────────────┘   └─────┘        └──┘               └──┘      └───┘
doc                                                                                   └───┘
txt                                                                                   └───┘
par                                                                                   └───┘
pid                                                                                       
st                                                                                   └────┘
128  
129  @[simp] lemma to_units_coe (s : S) : ((to_units s) : localization α S) = s := rfl
id                                         └──────┘     └──────────┘         └─┘
src                                         └──────┘      └──────────┘            └─┘
typ                                        └──────┘     └──────────┘         └─┘
doc    └──┘                                 └──────┘      └──────────┘
130  
131  section
132  variables (α S) (x y : α) (n : ℕ)
id                                  
src                                 
typ                                 
133  @[simp] lemma of_zero : (of 0 : localization α S) = 0 := rfl
id                            └┘     └──────────┘          └─┘
src                           └┘     └──────────┘            └─┘
typ                           └┘     └──────────┘          └─┘
doc    └──┘                   └┘     └──────────┘
134  @[simp] lemma of_one : (of 1 : localization α S) = 1 := rfl
id                           └┘     └──────────┘          └─┘
src                          └┘     └──────────┘            └─┘
typ                          └┘     └──────────┘          └─┘
doc    └──┘                  └┘     └──────────┘
135  @[simp] lemma of_add : (of (x + y) : localization α S) = of x + of y :=
id                           └┘        └──────────┘     └┘   └┘ 
src                          └┘          └──────────┘       └┘    └┘
typ                          └┘        └──────────┘     └┘   └┘ 
doc    └──┘                  └┘           └──────────┘        └┘     └┘
136  by apply is_ring_hom.map_add
id            └─────────────────┘
src     └────┘└─────────────────┘
typ     └────┘└─────────────────┘
doc     └────┘                   
txt     └────┘                   
par     └────┘                   
pid                             
st     └──────────────────────────
137  
src  
typ  
doc  
txt  
par  
pid  
st   
138  @[simp] lemma of_sub : (of (x - y) : localization α S) = of x - of y :=
id                           └┘        └──────────┘     └┘   └┘ 
src                          └┘          └──────────┘       └┘    └┘
typ                          └┘        └──────────┘     └┘   └┘ 
doc    └──┘                  └┘           └──────────┘        └┘     └┘
139  by apply is_ring_hom.map_sub
id            └─────────────────┘
src     └────┘└─────────────────┘
typ     └────┘└─────────────────┘
doc     └────┘└─────────────────┘
txt     └────┘                   
par     └────┘                   
pid                             
st     └──────────────────────────
140  
src  
typ  
doc  
txt  
par  
pid  
st   
141  @[simp] lemma of_mul : (of (x * y) : localization α S) = of x * of y :=
id                           └┘        └──────────┘     └┘   └┘ 
src                          └┘          └──────────┘       └┘    └┘
typ                          └┘        └──────────┘     └┘   └┘ 
doc    └──┘                  └┘           └──────────┘        └┘     └┘
142  by apply is_ring_hom.map_mul
id            └─────────────────┘
src     └────┘└─────────────────┘
typ     └────┘└─────────────────┘
doc     └────┘                   
txt     └────┘                   
par     └────┘                   
pid                             
st     └──────────────────────────
143  
src  
typ  
doc  
txt  
par  
pid  
st   
144  @[simp] lemma of_neg : (of (-x) : localization α S) = -of x :=
id                           └┘      └──────────┘     └┘ 
src                          └┘       └──────────┘       └┘
typ                          └┘      └──────────┘     └┘ 
doc    └──┘                  └┘        └──────────┘         └┘
145  by apply is_ring_hom.map_neg
id            └─────────────────┘
src     └────┘└─────────────────┘
typ     └────┘└─────────────────┘
doc     └────┘└─────────────────┘
txt     └────┘                   
par     └────┘                   
pid                             
st     └──────────────────────────
146  
src  
typ  
doc  
txt  
par  
pid  
st   
147  @[simp] lemma of_pow : (of (x ^ n) : localization α S) = (of x) ^ n :=
id                           └┘        └──────────┘      └┘    
src                          └┘          └──────────┘        └┘    
typ                          └┘        └──────────┘      └┘    
doc    └──┘                  └┘           └──────────┘         └┘
148  by apply is_semiring_hom.map_pow
id            └─────────────────────┘
src     └────┘└─────────────────────┘
typ     └────┘└─────────────────────┘
doc     └────┘                       
txt     └────┘                       
par     └────┘                       
pid                                 
st     └──────────────────────────────
149  
src  
typ  
doc  
txt  
par  
pid  
st   
150  @[simp] lemma of_is_unit (s : S) : is_unit (of s : localization α S) :=
id                                     └─────┘  └┘    └──────────┘  
src                                     └─────┘  └┘     └──────────┘
typ                                    └─────┘  └┘    └──────────┘  
doc    └──┘                             └─────┘  └┘     └──────────┘
151  is_unit_unit $ to_units s
id   └──────────┘   └──────┘ 
src  └──────────┘   └──────┘
typ  └──────────┘   └──────┘ 
doc                 └──────┘
152  
153  @[simp] lemma of_is_unit' (s ∈ S) : is_unit (of s : localization α S) :=
id                                     └─────┘  └┘    └──────────┘  
src                                      └─────┘  └┘     └──────────┘
typ                                    └─────┘  └┘    └──────────┘  
doc    └──┘                              └─────┘  └┘     └──────────┘
154  is_unit_unit $ to_units ⟨s, ‹s ∈ S›⟩
id   └──────────┘   └──────┘      
src  └──────────┘   └──────┘         
typ  └──────────┘   └──────┘      
doc                 └──────┘          
155  
156  @[simp] lemma coe_zero : ((0 : α) : localization α S) = 0 := rfl
id                                      └──────────┘          └─┘
src                                      └──────────┘            └─┘
typ                                     └──────────┘          └─┘
doc    └──┘                              └──────────┘
157  @[simp] lemma coe_one : ((1 : α) : localization α S) = 1 := rfl
id                                     └──────────┘          └─┘
src                                     └──────────┘            └─┘
typ                                    └──────────┘          └─┘
doc    └──┘                             └──────────┘
158  @[simp] lemma coe_add : (↑(x + y) : localization α S) = x + y := of_add _ _ _ _
id                                   └──────────┘           └────┘
src                                    └──────────┘               └────┘
typ                                  └──────────┘           └────┘
doc    └──┘                              └──────────┘
159  @[simp] lemma coe_sub : (↑(x - y) : localization α S) = x - y := of_sub _ _ _ _
id                                   └──────────┘           └────┘
src                                    └──────────┘               └────┘
typ                                  └──────────┘           └────┘
doc    └──┘                              └──────────┘
160  @[simp] lemma coe_mul : (↑(x * y) : localization α S) = x * y := of_mul _ _ _ _
id                                   └──────────┘           └────┘
src                                    └──────────┘               └────┘
typ                                  └──────────┘           └────┘
doc    └──┘                              └──────────┘
161  @[simp] lemma coe_neg : (↑(-x) : localization α S) = -x := of_neg _ _ _
id                                 └──────────┘         └────┘
src                                 └──────────┘            └────┘
typ                                └──────────┘         └────┘
doc    └──┘                           └──────────┘
162  @[simp] lemma coe_pow : (↑(x ^ n) : localization α S) = x ^ n := of_pow _ _ _ _
id                                   └──────────┘           └────┘
src                                    └──────────┘               └────┘
typ                                  └──────────┘           └────┘
doc    └──┘                              └──────────┘
163  @[simp] lemma coe_is_unit (s : S) : is_unit (s : localization α S) := of_is_unit _ _ _
id                                      └─────┘     └──────────┘       └────────┘
src                                      └─────┘      └──────────┘         └────────┘
typ                                     └─────┘     └──────────┘       └────────┘
doc    └──┘                              └─────┘      └──────────┘
164  @[simp] lemma coe_is_unit' (s ∈ S) : is_unit (s : localization α S) := of_is_unit' _ _ _ ‹s ∈ S›
id                                      └─────┘     └──────────┘       └─────────┘         
src                                       └─────┘      └──────────┘         └─────────┘           
typ                                     └─────┘     └──────────┘       └─────────┘         
doc    └──┘                               └─────┘      └──────────┘                                
165  end
166  
167  @[simp] lemma mk_self {x : α} {hx : x ∈ S} :
id                                        
src                                        
typ                                       
doc    └──┘
168    (mk x ⟨x, hx⟩ : localization α S) = 1 :=
id      └┘     └┘    └──────────┘    
src     └┘             └──────────┘      
typ     └┘     └┘    └──────────┘    
doc                    └──────────┘
169  quotient.sound ⟨1, is_submonoid.one_mem S,
id   └────────────┘     └──────────────────┘ 
src  └────────────┘     └──────────────────┘
typ  └────────────┘     └──────────────────┘ 
170  by simp only [subtype.coe_mk, is_submonoid.coe_one, mul_one, one_mul, sub_self]⟩
id                 └────────────┘  └──────────────────┘  └─────┘  └─────┘  └──────┘
src     └─────────┘└────────────┘└┘└──────────────────┘└┘└─────┘└┘└─────┘└┘└──────┘
typ     └─────────┘└────────────┘└┘└──────────────────┘└┘└─────┘└┘└─────┘└┘└──────┘
doc     └─────────┘              └┘└──────────────────┘└┘       └┘       └┘        
txt     └─────────┘              └┘                    └┘       └┘       └┘        
par     └─────────┘              └┘                    └┘       └┘       └┘        
pid         └──┘└┘              └┘                    └┘       └┘       └┘        
st     └───────────────────────────────────────────────────────────────────────────┘
171  
172  @[simp] lemma mk_self' {s : S} :
id                               
typ                              
doc    └──┘
173    (mk s s : localization α S) = 1 :=
id      └┘     └──────────┘    
src     └┘       └──────────┘      
typ     └┘     └──────────┘    
doc              └──────────┘
174  by cases s; exact mk_self
id                    └─────┘
src     └────┘   └────┘└─────┘
typ     └────┘  └────┘└─────┘
doc     └────┘   └────┘       
txt     └────┘   └────┘       
par     └────┘   └────┘       
pid                         
st     └───────────────────────
175  
src  
typ  
doc  
txt  
par  
pid  
st   
176  @[simp] lemma mk_self'' {s : S} :
id                                
typ                               
doc    └──┘
177    (mk s.1 s : localization α S) = 1 :=
id      └┘      └──────────┘    
src     └┘        └──────────┘      
typ     └┘      └──────────┘    
doc                └──────────┘
178  mk_self'
id   └──────┘
src  └──────┘
typ  └──────┘
179  
180  @[simp] lemma coe_mul_mk (x y : α) (s : S) :
id                                          
typ                                         
doc    └──┘
181    ↑x * mk y s = mk (x * y) s :=
id       └┘    └┘      
src       └┘      └┘    
typ      └┘    └┘      
182  quotient.sound $ r_of_eq $ by rw one_mul
id   └────────────┘   └─────┘         └─────┘
src  └────────────┘   └─────┘      └─┘└─────┘
typ  └────────────┘   └─────┘      └─┘└─────┘
doc                                └─┘       
txt                                └─┘       
par                                └─┘       
pid                                         
st                                └───────────
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  lemma mk_eq_mul_mk_one (r : α) (s : S) :
id                                      
typ                                     
185    mk r s = r * mk 1 s :=
id     └┘      └┘   
src    └┘         └┘
typ    └┘      └┘   
186  by rw [coe_mul_mk, mul_one]
id          └────────┘  └─────┘
src     └──┘└────────┘└┘└─────┘└─
typ     └──┘└────────┘└┘└─────┘└─
doc     └──┘          └┘       └─
txt     └──┘          └┘       └─
par     └──┘          └┘       └─
pid       └┘          └┘       
st     └─────────────┘└───────┘
187  
src  
typ  
doc  
txt  
par  
pid  
st   
188  @[simp] lemma mk_mul_mk (x y : α) (s t : S) :
id                                           
typ                                          
doc    └──┘
189    mk x s * mk y t = mk (x * y) (s * t) := rfl
id     └┘    └┘    └┘              └─┘
src    └┘      └┘      └┘                  └─┘
typ    └┘    └┘    └┘              └─┘
190  
191  @[simp] lemma mk_mul_cancel_left (r : α) (s : S) :
id                                                
typ                                               
doc    └──┘
192    mk (↑s * r) s = r :=
id     └┘        
src    └┘          
typ    └┘        
193  by rw [mk_eq_mul_mk_one, mul_comm ↑s, coe_mul,
id          └──────────────┘  └──────┘   └─────┘
src     └──┘└──────────────┘└┘└──────┘ └┘└─────┘└─
typ     └──┘└──────────────┘└┘└──────┘└┘└─────┘└─
doc     └──┘                └┘          └┘       └─
txt     └──┘                └┘          └┘       └─
par     └──┘                └┘          └┘       └─
pid       └┘                └┘          └┘       └─
st     └───────────────────┘└───────────┘└───────┘└─
194         mul_assoc, ← mk_eq_mul_mk_one, mk_self', mul_one]
id          └───────┘    └──────────────┘  └──────┘  └─────┘
src  ──────┘└───────┘└──┘└──────────────┘└┘└──────┘└┘└─────┘└─
typ  ──────┘└───────┘└──┘└──────────────┘└┘└──────┘└┘└─────┘└─
doc  ──────┘         └──┘                └┘        └┘       └─
txt  ──────┘         └──┘                └┘        └┘       └─
par  ──────┘         └──┘                └┘        └┘       └─
pid  ──────┘         └──┘                └┘        └┘       
st   ───────────────┘└──────────────────┘└────────┘└───────┘
195  
src  
typ  
doc  
txt  
par  
pid  
st   
196  @[simp] lemma mk_mul_cancel_right (r : α) (s : S) :
id                                                 
typ                                                
doc    └──┘
197    mk (r * s) s = r :=
id     └┘        
src    └┘          
typ    └┘        
198  by rw [mul_comm, mk_mul_cancel_left]
id          └──────┘  └────────────────┘
src     └──┘└──────┘└┘└────────────────┘└─
typ     └──┘└──────┘└┘└────────────────┘└─
doc     └──┘        └┘                  └─
txt     └──┘        └┘                  └─
par     └──┘        └┘                  └─
pid       └┘        └┘                  
st     └───────────┘└──────────────────┘
199  
src  
typ  
doc  
txt  
par  
pid  
st   
200  @[simp] lemma mk_eq (r : α) (s : S) :
id                                   
typ                                  
doc    └──┘
201    mk r s = r * ((to_units s)⁻¹ : units _) :=
id     └┘        └──────┘  └┘   └───┘
src    └┘           └──────┘   └┘   └───┘
typ    └┘        └──────┘  └┘   └───┘
doc                   └──────┘
202  quotient.sound $ by simp
id   └────────────┘
src  └────────────┘      └────
typ  └────────────┘      └────
doc                      └────
txt                      └────
par                      └────
pid                          
st                      └─────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204  @[elab_as_eliminator]
doc    └────────────────┘
205  protected theorem induction_on {C : localization α S → Prop} (x : localization α S)
id                                       └──────────┘                └──────────┘  
src                                      └──────────┘                  └──────────┘
typ                                      └──────────┘                └──────────┘  
doc                                      └──────────┘                  └──────────┘
206    (ih : ∀ r s, C (mk r s : localization α S)) : C x :=
id                  └┘     └──────────┘        
src                    └┘       └──────────┘
typ                 └┘     └──────────┘        
doc                             └──────────┘
207  by rcases x with ⟨r, s⟩; exact ih r s
id                                 └┘  
src     └─────┘ └──────────┘  └────┘    
typ     └─────┘└──────────┘  └────┘└┘
doc     └─────┘ └──────────┘  └────┘    
txt     └─────┘ └──────────┘  └────┘    
par     └─────┘ └──────────┘  └────┘    
pid            └──────────┘           
st     └───────────────────────────────────
208  
src  
typ  
doc  
txt  
par  
pid  
st   
209  section
210  variables {β : Type v} [comm_ring β] {T : set β} [is_submonoid T] (f : α → β) [is_ring_hom f]
id                           └───────┘         └─┘     └──────────┘                 └─────────┘
src                          └───────┘         └─┘     └──────────┘                 └─────────┘
typ                          └───────┘         └─┘     └──────────┘                 └─────────┘
doc                                                    └──────────┘                 └─────────┘
211  
212  @[elab_with_expected_type]
doc    └─────────────────────┘
213  def lift' (g : S → units β) (hg : ∀ s, (g s : β) = f s) (x : localization α S) : β :=
id                     └───┘                             └──────────┘      
src                     └───┘                                    └──────────┘
typ                    └───┘                             └──────────┘      
doc                                                               └──────────┘
214  quotient.lift_on x (λ p, f p.1 * ((g p.2)⁻¹ : units β)) $ λ ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨t, hts, ht⟩,
id   └──────────────┘                └┘   └───┘        └┘  └┘  └┘  └┘    └─┘
src  └──────────────┘                      └┘   └───┘
typ  └──────────────┘                └┘   └───┘        └┘  └┘  └┘  └┘    └─┘
215  show f r₁ * ↑(g s₁)⁻¹ = f r₂ * ↑(g s₂)⁻¹, from
id                  └┘            └┘
src                   └┘              └┘
typ                 └┘            └┘
216  calc  f r₁ * ↑(g s₁)⁻¹
id                   └┘
src                    └┘
typ                  └┘
217      = (f r₁ * g s₂ + ((g s₁ * f r₂ - g s₂ * f r₁) * g ⟨t, hts⟩) * ↑(g ⟨t, hts⟩)⁻¹)
id                                                                  └┘
src                                                                         └┘
typ                                                                 └┘
218        * ↑(g s₁)⁻¹ * ↑(g s₂)⁻¹ :
id               └┘       └┘
src               └┘        └┘
typ              └┘       └┘
219    by simp only [hg, subtype.coe_mk, (is_ring_hom.map_mul f).symm, (is_ring_hom.map_sub f).symm,
id                   └┘  └────────────┘   └─────────────────┘          └─────────────────┘ 
src       └─────────┘  └┘└────────────┘└┘ └─────────────────┘ └──────┘ └─────────────────┘ └───────
typ       └─────────┘└┘└┘└────────────┘└┘ └─────────────────┘└──────┘ └─────────────────┘└───────
doc       └─────────┘  └┘              └┘                     └──────┘ └─────────────────┘ └───────
txt       └─────────┘  └┘              └┘                     └──────┘                     └───────
par       └─────────┘  └┘              └┘                     └──────┘                     └───────
pid           └──┘└┘  └┘              └┘                     └──────┘                     └───────
st       └───────────────────────────────────────────────────────────────────────────────────────────
220                  ht, is_ring_hom.map_zero f, zero_mul, add_zero];
id                   └┘  └──────────────────┘   └──────┘  └──────┘
src  ───────────────┘  └┘└──────────────────┘ └┘└──────┘└┘└──────┘
typ  ───────────────┘└┘└┘└──────────────────┘└┘└──────┘└┘└──────┘
doc  ───────────────┘  └┘└──────────────────┘ └┘        └┘        
txt  ───────────────┘  └┘                     └┘        └┘        
par  ───────────────┘  └┘                     └┘        └┘        
pid  ───────────────┘  └┘                     └┘        └┘        
st   ─────────────────────────────────────────────────────────────────
221       rw [is_ring_hom.map_mul f, ← hg, mul_right_comm,
id            └─────────────────┘     └┘  └────────────┘
src       └──┘└─────────────────┘ └──┘  └┘└────────────┘└─
typ       └──┘└─────────────────┘└──┘└┘└┘└────────────┘└─
doc       └──┘                    └──┘  └┘              └─
txt       └──┘                    └──┘  └┘              └─
par       └──┘                    └──┘  └┘              └─
pid         └┘                    └──┘  └┘              └─
st   ────────┘└───────────────────┘└────┘└──────────────┘└─
222           mul_assoc (f r₁), ← units.coe_mul, mul_inv_self];
id            └───────┘   └┘     └───────────┘  └──────────┘
src  ────────┘└───────┘    └───┘└───────────┘└┘└──────────┘
typ  ────────┘└───────┘ └┘└───┘└───────────┘└┘└──────────┘
doc  ────────┘             └───┘             └┘            
txt  ────────┘             └───┘             └┘            
par  ────────┘             └───┘             └┘            
pid  ────────┘             └───┘             └┘            
st   ────────────────────────┘└───────────────┘└────────────┘└─
223       rw [units.coe_one, mul_one]
id            └───────────┘  └─────┘
src       └──┘└───────────┘└┘└─────┘└┘
typ       └──┘└───────────┘└┘└─────┘└┘
doc       └──┘             └┘       └┘
txt       └──┘             └┘       └┘
par       └──┘             └┘       └┘
pid         └┘             └┘       
st   ────────┘└───────────┘└───────┘
224  ... = f r₂ * ↑(g s₂)⁻¹ :
id                   └┘
src                    └┘
typ                  └┘
225    by rw [mul_assoc, mul_assoc, ← units.coe_mul, mul_inv_self, units.coe_one,
id            └───────┘  └───────┘    └───────────┘  └──────────┘  └───────────┘
src       └──┘└───────┘└┘└───────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
typ       └──┘└───────┘└┘└───────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
doc       └──┘         └┘         └──┘             └┘            └┘             └─
txt       └──┘         └┘         └──┘             └┘            └┘             └─
par       └──┘         └┘         └──┘             └┘            └┘             └─
pid         └┘         └┘         └──┘             └┘            └┘             └─
st       └────────────┘└─────────┘└───────────────┘└────────────┘└─────────────┘└─
226           mul_one, mul_comm ↑(g s₂), add_sub_cancel'_right];
id            └─────┘  └──────┘   └┘   └───────────────────┘
src  ────────┘└─────┘└┘└──────┘    └─┘└───────────────────┘
typ  ────────┘└─────┘└┘└──────┘ └┘└─┘└───────────────────┘
doc  ────────┘       └┘             └─┘                     
txt  ────────┘       └┘             └─┘                     
par  ────────┘       └┘             └─┘                     
pid  ────────┘       └┘             └─┘                     
st   ───────────────┘└────────────────┘└─────────────────────┘└─
227       rw [mul_comm ↑(g s₁), ← mul_assoc, mul_assoc (f r₂), ← units.coe_mul,
id            └──────┘    └┘     └───────┘  └───────┘   └┘     └───────────┘
src       └──┘└──────┘     └───┘└───────┘└┘└───────┘    └───┘└───────────┘└─
typ       └──┘└──────┘  └┘└───┘└───────┘└┘└───────┘ └┘└───┘└───────────┘└─
doc       └──┘             └───┘         └┘             └───┘             └─
txt       └──┘             └───┘         └┘             └───┘             └─
par       └──┘             └───┘         └┘             └───┘             └─
pid         └┘             └───┘         └┘             └───┘             └─
st   ────────┘└──────────────┘└───────────┘└────────────────┘└───────────────┘└─
228           mul_inv_self, units.coe_one, mul_one]
id            └──────────┘  └───────────┘  └─────┘
src  ────────┘└──────────┘└┘└───────────┘└┘└─────┘└─
typ  ────────┘└──────────┘└┘└───────────┘└┘└─────┘└─
doc  ────────┘            └┘             └┘       └─
txt  ────────┘            └┘             └┘       └─
par  ────────┘            └┘             └┘       └─
pid  ────────┘            └┘             └┘       
st   ────────────────────┘└─────────────┘└───────┘
229  
src  
typ  
doc  
txt  
par  
pid  
st   
230  instance lift'.is_ring_hom (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id                                      └───┘                      
src                                      └───┘                         
typ                                     └───┘                      
231    is_ring_hom (localization.lift' f g hg) :=
id     └─────────┘  └────────────────┘   └┘
src    └─────────┘  └────────────────┘
typ    └─────────┘  └────────────────┘   └┘
doc    └─────────┘
232  { map_one := have g 1 = 1, from units.ext (by rw hg; exact is_ring_hom.map_one f),
id                                 └───────┘        └┘        └─────────────────┘ 
src                                 └───────┘     └─┘    └────┘└─────────────────┘
typ                                └───────┘     └─┘└┘  └────┘└─────────────────┘
doc                                                └─┘    └────┘                   
txt                                                └─┘    └────┘                   
par                                                └─┘    └────┘                   
pid                                                                              
st                                                └─────────────────────────────────┘
233      show f 1 * ↑(g 1)⁻¹ = 1, by rw [this, one_inv, units.coe_one, mul_one, is_ring_hom.map_one f],
id                    └┘            └──┘  └─────┘  └───────────┘  └─────┘  └─────────────────┘ 
src                     └┘        └──┘    └┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘ 
typ                   └┘        └──┘└──┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘
doc                                  └──┘    └┘       └┘             └┘       └┘                    
txt                                  └──┘    └┘       └┘             └┘       └┘                    
par                                  └──┘    └┘       └┘             └┘       └┘                    
pid                                    └┘    └┘       └┘             └┘       └┘                    
st                                  └───────┘└───────┘└─────────────┘└───────┘└─────────────────────┘
234    map_mul := λ x y, localization.induction_on x $ λ r₁ s₁,
id                     └───────────────────────┘      └┘ └┘
src                      └───────────────────────┘
typ                    └───────────────────────┘      └┘ └┘
235      localization.induction_on y $ λ r₂ s₂,
id       └───────────────────────┘      └┘ └┘
src      └───────────────────────┘
typ      └───────────────────────┘      └┘ └┘
236      have g (s₁ * s₂) = g s₁ * g s₂,
id              └┘  └┘    └┘   └┘
src                            
typ             └┘  └┘    └┘   └┘
237        from units.ext (by simp only [hg, units.coe_mul]; exact is_ring_hom.map_mul f),
id              └───────┘                └┘  └───────────┘         └─────────────────┘ 
src             └───────┘     └─────────┘  └┘└───────────┘  └────┘└─────────────────┘
typ             └───────┘     └─────────┘└┘└┘└───────────┘  └────┘└─────────────────┘
doc                           └─────────┘  └┘               └────┘                   
txt                           └─────────┘  └┘               └────┘                   
par                           └─────────┘  └┘               └────┘                   
pid                               └──┘└┘  └┘                                       
st                           └─────────────────────────────────────────────────────────┘
238      show _ * ↑(g (_ * _))⁻¹ = (_ * _) * (_ * _),
id                        └┘             
src                        └┘             
typ                       └┘             
239      by simp only [subtype.coe_mk, mul_one, one_mul, subtype.coe_eta, this, mul_inv_rev];
id                     └────────────┘  └─────┘  └─────┘  └─────────────┘  └──┘  └─────────┘
src         └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘    └┘└─────────┘
typ         └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘└──┘└┘└─────────┘
doc         └─────────┘              └┘       └┘       └┘               └┘    └┘           
txt         └─────────┘              └┘       └┘       └┘               └┘    └┘           
par         └─────────┘              └┘       └┘       └┘               └┘    └┘           
pid             └──┘└┘              └┘       └┘       └┘               └┘    └┘           
st         └──────────────────────────────────────────────────────────────────────────────────
240         rw [is_ring_hom.map_mul f, units.coe_mul, ← mul_assoc, ← mul_assoc];
id              └─────────────────┘   └───────────┘    └───────┘    └───────┘
src         └──┘└─────────────────┘ └┘└───────────┘└──┘└───────┘└──┘└───────┘
typ         └──┘└─────────────────┘└┘└───────────┘└──┘└───────┘└──┘└───────┘
doc         └──┘                    └┘             └──┘         └──┘         
txt         └──┘                    └┘             └──┘         └──┘         
par         └──┘                    └┘             └──┘         └──┘         
pid           └┘                    └┘             └──┘         └──┘         
st   ──────────┘└───────────────────┘└─────────────┘└───────────┘└───────────┘└─
241         simp only [mul_right_comm],
id                     └────────────┘
src         └─────────┘└────────────┘
typ         └─────────┘└────────────┘
doc         └─────────┘              
txt         └─────────┘              
par         └─────────┘              
pid             └──┘└┘              
st   ────────────────────────────────┘
242    map_add := λ x y, localization.induction_on x $ λ r₁ s₁,
id                     └───────────────────────┘      └┘ └┘
src                      └───────────────────────┘
typ                    └───────────────────────┘      └┘ └┘
243      localization.induction_on y $ λ r₂ s₂,
id       └───────────────────────┘      └┘ └┘
src      └───────────────────────┘
typ      └───────────────────────┘      └┘ └┘
244      have g (s₁ * s₂) = g s₁ * g s₂,
id              └┘  └┘    └┘   └┘
src                            
typ             └┘  └┘    └┘   └┘
245        from units.ext (by simp only [hg, units.coe_mul]; exact is_ring_hom.map_mul f),
id              └───────┘                └┘  └───────────┘         └─────────────────┘ 
src             └───────┘     └─────────┘  └┘└───────────┘  └────┘└─────────────────┘
typ             └───────┘     └─────────┘└┘└┘└───────────┘  └────┘└─────────────────┘
doc                           └─────────┘  └┘               └────┘                   
txt                           └─────────┘  └┘               └────┘                   
par                           └─────────┘  └┘               └────┘                   
pid                               └──┘└┘  └┘                                       
st                           └─────────────────────────────────────────────────────────┘
246      show _ * ↑(g (_ * _))⁻¹ = _ * _ + _ * _,
id                        └┘          
src                        └┘          
typ                       └┘          
247      by simp only [subtype.coe_mk, mul_one, one_mul, subtype.coe_eta, this, mul_inv_rev];
id                     └────────────┘  └─────┘  └─────┘  └─────────────┘  └──┘  └─────────┘
src         └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘    └┘└─────────┘
typ         └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘└──┘└┘└─────────┘
doc         └─────────┘              └┘       └┘       └┘               └┘    └┘           
txt         └─────────┘              └┘       └┘       └┘               └┘    └┘           
par         └─────────┘              └┘       └┘       └┘               └┘    └┘           
pid             └──┘└┘              └┘       └┘       └┘               └┘    └┘           
st         └──────────────────────────────────────────────────────────────────────────────────
248         simp only [is_ring_hom.map_mul f, is_ring_hom.map_add f, add_mul, (hg _).symm];
id                     └─────────────────┘   └─────────────────┘   └─────┘   └┘
src         └─────────┘└─────────────────┘ └┘└─────────────────┘ └┘└─────┘└┘   └───────┘
typ         └─────────┘└─────────────────┘└┘└─────────────────┘└┘└─────┘└┘ └┘└───────┘
doc         └─────────┘                    └┘                    └┘       └┘   └───────┘
txt         └─────────┘                    └┘                    └┘       └┘   └───────┘
par         └─────────┘                    └┘                    └┘       └┘   └───────┘
pid             └──┘└┘                    └┘                    └┘       └┘   └───────┘
st   ───────────────────────────────────────────────────────────────────────────────────────
249         simp only [mul_assoc, mul_comm, mul_left_comm, (units.coe_mul _ _).symm];
id                     └───────┘  └──────┘  └───────────┘   └───────────┘
src         └─────────┘└───────┘└┘└──────┘└┘└───────────┘└┘ └───────────┘└─────────┘
typ         └─────────┘└───────┘└┘└──────┘└┘└───────────┘└┘ └───────────┘└─────────┘
doc         └─────────┘         └┘        └┘             └┘              └─────────┘
txt         └─────────┘         └┘        └┘             └┘              └─────────┘
par         └─────────┘         └┘        └┘             └┘              └─────────┘
pid             └──┘└┘         └┘        └┘             └┘              └─────────┘
st   ─────────────────────────────────────────────────────────────────────────────────
250         rw [mul_inv_cancel_left, mul_left_comm, ← mul_assoc, mul_inv_cancel_right, add_comm] }
id              └─────────────────┘  └───────────┘    └───────┘  └──────────────────┘  └──────┘
src         └──┘└─────────────────┘└┘└───────────┘└──┘└───────┘└┘└──────────────────┘└┘└──────┘└┘
typ         └──┘└─────────────────┘└┘└───────────┘└──┘└───────┘└┘└──────────────────┘└┘└──────┘└┘
doc         └──┘                   └┘             └──┘         └┘                    └┘        └┘
txt         └──┘                   └┘             └──┘         └┘                    └┘        └┘
par         └──┘                   └┘             └──┘         └┘                    └┘        └┘
pid           └┘                   └┘             └──┘         └┘                    └┘        
st   ──────────┘└─────────────────┘└─────────────┘└───────────┘└────────────────────┘└────────┘
251  
252  noncomputable def lift (h : ∀ s ∈ S, is_unit (f s)) :
id                                      └─────┘   
src                                      └─────┘
typ                                     └─────┘   
doc                                       └─────┘
253    localization α S → β :=
id     └──────────┘     
src    └──────────┘
typ    └──────────┘     
doc    └──────────┘
254  localization.lift' f (λ s, classical.some $ h s.1 s.2)
id   └────────────────┘       └────────────┘      
src  └────────────────┘         └────────────┘         
typ  └────────────────┘       └────────────┘      
255    (λ s, by rw [← classical.some_spec (h s.1 s.2)]; refl)
id                   └─────────────────┘       
src             └────┘└─────────────────┘   └─┘ └──┘  └──┘
typ            └────┘└─────────────────┘  └─┘└──┘  └──┘
doc             └────┘                      └─┘ └──┘  └──┘
txt             └────┘                      └─┘ └──┘  └──┘
par             └────┘                      └─┘ └──┘  └──┘
pid               └──┘                      └─┘ └──┘
st             └────────────────────────────────────┘└────┘
256  
257  instance lift.is_ring_hom (h : ∀ s ∈ S, is_unit (f s)) :
id                                         └─────┘   
src                                          └─────┘
typ                                        └─────┘   
doc                                          └─────┘
258    is_ring_hom (lift f h) :=
id     └─────────┘  └──┘  
src    └─────────┘  └──┘
typ    └─────────┘  └──┘  
doc    └─────────┘
259  lift'.is_ring_hom _ _ _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
260  
261  @[simp] lemma lift'_mk (g : S → units β) (hg : ∀ s, (g s : β) = f s) (r : α) (s : S) :
id                                  └───┘                                    
src                                  └───┘                         
typ                                 └───┘                                    
doc    └──┘
262    lift' f g hg (mk r s) = f r * ↑(g s)⁻¹ := rfl
id     └───┘   └┘  └┘           └┘    └─┘
src    └───┘         └┘                 └┘    └─┘
typ    └───┘   └┘  └┘           └┘    └─┘
263  
264  @[simp] lemma lift'_of (g : S → units β) (hg : ∀ s, (g s : β) = f s) (a : α) :
id                                  └───┘                             
src                                  └───┘                         
typ                                 └───┘                             
doc    └──┘
265    lift' f g hg (of a) = f a :=
id     └───┘   └┘  └┘     
src    └───┘         └┘    
typ    └───┘   └┘  └┘     
doc                  └┘
266  have g 1 = 1, from units.ext_iff.2 $ by simp [hg, is_ring_hom.map_one f],
id                    └───────────┘             └┘  └─────────────────┘ 
src                    └───────────┘       └────┘  └┘└─────────────────┘ 
typ                   └───────────┘       └────┘└┘└┘└─────────────────┘
doc                                          └────┘  └┘                    
txt                                          └────┘  └┘                    
par                                          └────┘  └┘                    
pid                                                └┘                    
st                                          └───────────────────────────────┘
267  by simp [lift', quotient.lift_on_beta, of, mk, this]
id            └───┘  └───────────────────┘  └┘  └┘  └──┘
src     └────┘└───┘└┘└───────────────────┘└┘└┘└┘└┘└┘    └─
typ     └────┘└───┘└┘└───────────────────┘└┘└┘└┘└┘└┘└──┘└─
doc     └────┘     └┘                     └┘└┘└┘  └┘    └─
txt     └────┘     └┘                     └┘  └┘  └┘    └─
par     └────┘     └┘                     └┘  └┘  └┘    └─
pid              └┘                     └┘  └┘  └┘    
st     └──────────────────────────────────────────────────
268  
src  
typ  
doc  
txt  
par  
pid  
st   
269  @[simp] lemma lift'_coe (g : S → units β) (hg : ∀ s, (g s : β) = f s) (a : α) :
id                                   └───┘                             
src                                   └───┘                         
typ                                  └───┘                             
doc    └──┘
270    lift' f g hg a = f a := lift'_of _ _ _ _
id     └───┘   └┘        └──────┘
src    └───┘                  └──────┘
typ    └───┘   └┘        └──────┘
271  
272  @[simp] lemma lift_of (h : ∀ s ∈ S, is_unit (f s)) (a : α) :
id                                     └─────┘           
src                                      └─────┘
typ                                    └─────┘           
doc    └──┘                              └─────┘
273    lift f h (of a) = f a := lift'_of _ _ _ _
id     └──┘    └┘         └──────┘
src    └──┘      └┘            └──────┘
typ    └──┘    └┘         └──────┘
doc              └┘
274  
275  @[simp] lemma lift_coe (h : ∀ s ∈ S, is_unit (f s)) (a : α) :
id                                      └─────┘           
src                                       └─────┘
typ                                     └─────┘           
doc    └──┘                               └─────┘
276    lift f h a = f a := lift'_of _ _ _ _
id     └──┘          └──────┘
src    └──┘               └──────┘
typ    └──┘          └──────┘
277  
278  @[simp] lemma lift'_comp_of (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id                                       └───┘                      
src                                       └───┘                         
typ                                      └───┘                      
doc    └──┘
279    lift' f g hg ∘ of = f := funext $ λ a, lift'_of _ _ _ a
id     └───┘   └┘  └┘      └────┘       └──────┘       
src    └───┘         └┘       └────┘        └──────┘
typ    └───┘   └┘  └┘      └────┘       └──────┘       
doc                   └┘
280  
281  @[simp] lemma lift_comp_of (h : ∀ s ∈ S, is_unit (f s)) :
id                                          └─────┘   
src                                           └─────┘
typ                                         └─────┘   
doc    └──┘                                   └─────┘
282    lift f h ∘ of = f := lift'_comp_of _ _ _
id     └──┘    └┘      └───────────┘
src    └──┘      └┘       └───────────┘
typ    └──┘    └┘      └───────────┘
doc               └┘
283  
284  @[simp] lemma lift'_apply_coe (f : localization α S → β) [is_ring_hom f]
id                                      └──────────┘        └─────────┘ 
src                                     └──────────┘           └─────────┘
typ                                     └──────────┘        └─────────┘ 
doc    └──┘                             └──────────┘           └─────────┘
285    (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id             └───┘                      
src             └───┘                         
typ            └───┘                      
286    lift' (λ a : α, f a) g hg = f :=
id     └───┘              └┘  
src    └───┘                     
typ    └───┘              └┘  
287  have g = (λ s, (units.map' f : units (localization α S) → units β) (to_units s)),
id                └────────┘    └───┘  └──────────┘      └───┘    └──────┘ 
src                 └────────┘     └───┘  └──────────┘        └───┘     └──────┘
typ               └────────┘    └───┘  └──────────┘      └───┘    └──────┘ 
doc                  └────────┘            └──────────┘                  └──────┘
288    from funext $ λ x, units.ext $ (hg x).symm ▸ rfl,
id          └────┘       └───────┘    └┘  └──┘   └─┘
src         └────┘        └───────┘         └──┘   └─┘
typ         └────┘       └───────┘    └┘  └──┘   └─┘
289  funext $ λ x, localization.induction_on x
id   └────┘       └───────────────────────┘ 
src  └────┘        └───────────────────────┘
typ  └────┘       └───────────────────────┘ 
290    (λ r s, by subst this; rw [lift'_mk, ← (units.map' f).map_inv, units.coe_map'];
id                    └──┘      └──────┘     └────────┘            └────────────┘
src               └────┘      └──┘└──────┘└──┘ └────────┘ └─────────┘└────────────┘
typ             └────┘└──┘  └──┘└──────┘└──┘ └────────┘└─────────┘└────────────┘
doc               └────┘      └──┘        └──┘ └────────┘ └─────────┘              
txt               └────┘      └──┘        └──┘            └─────────┘              
par               └────┘      └──┘        └──┘            └─────────┘              
pid                            └┘        └──┘            └─────────┘              
st               └───────────────┘└──────┘└───────────────────────┘└───────────────┘└─
291      simp [is_ring_hom.map_mul f])
id             └─────────────────┘ 
src      └────┘└─────────────────┘ 
typ      └────┘└─────────────────┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                              
st   ───────────────────────────────┘
292  
293  @[simp] lemma lift_apply_coe (f : localization α S → β) [is_ring_hom f] :
id                                     └──────────┘        └─────────┘ 
src                                    └──────────┘           └─────────┘
typ                                    └──────────┘        └─────────┘ 
doc    └──┘                            └──────────┘           └─────────┘
294    lift (λ a : α, f a)
id     └──┘           
src    └──┘
typ    └──┘           
295      (λ s hs, is_unit.map' f (is_unit_unit (to_units ⟨s, hs⟩))) = f :=
id           └┘  └──────────┘   └──────────┘  └──────┘    └┘      
src               └──────────┘    └──────────┘  └──────┘            
typ          └┘  └──────────┘   └──────────┘  └──────┘    └┘      
doc                                             └──────┘
296  by rw [lift, lift'_apply_coe]
id          └──┘  └─────────────┘
src     └──┘└──┘└┘└─────────────┘└─
typ     └──┘└──┘└┘└─────────────┘└─
doc     └──┘    └┘               └─
txt     └──┘    └┘               └─
par     └──┘    └┘               └─
pid       └┘    └┘               
st     └───────┘└───────────────┘
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  /-- Function extensionality for localisations:
299   two functions are equal if they agree on elements that are coercions.-/
300  protected lemma funext (f g : localization α S → β) [is_ring_hom f] [is_ring_hom g]
id                                 └──────────┘        └─────────┘    └─────────┘ 
src                                └──────────┘           └─────────┘     └─────────┘
typ                                └──────────┘        └─────────┘    └─────────┘ 
doc                                └──────────┘           └─────────┘     └─────────┘
301    (h : ∀ a : α, f a = g a) : f = g :=
id                            
src                                
typ                           
302  begin
st   └─────
303    rw [← lift_apply_coe f, ← lift_apply_coe g],
id           └────────────┘     └────────────┘ 
src    └────┘└────────────┘ └──┘└────────────┘ 
typ    └────┘└────────────┘└──┘└────────────┘
doc    └────┘               └──┘               
txt    └────┘               └──┘               
par    └────┘               └──┘               
pid      └──┘               └──┘               
st   ───────────────────────┘└──────────────────┘└──
304    congr' 1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
305    exact funext h
id           └────┘ 
src    └────┘└────┘ 
typ    └────┘└────┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid                
st   ────────────────┘
306  end
st   └─┘
307  
308  variables {α S T}
309  
310  def map (hf : ∀ s ∈ S, f s ∈ T) : localization α S → localization β T :=
id                               └──────────┘     └──────────┘  
src                                   └──────────┘       └──────────┘
typ                              └──────────┘     └──────────┘  
doc                                    └──────────┘       └──────────┘
311  lift' (of ∘ f) (to_units ∘ subtype.map f hf) (λ s, rfl)
id   └───┘  └┘     └──────┘  └─────────┘  └┘       └─┘
src  └───┘  └┘      └──────┘  └─────────┘             └─┘
typ  └───┘  └┘     └──────┘  └─────────┘  └┘       └─┘
doc         └┘       └──────┘   └─────────┘
312  
313  instance map.is_ring_hom (hf : ∀ s ∈ S, f s ∈ T) : is_ring_hom (map f hf) :=
id                                                └─────────┘  └─┘  └┘
src                                                    └─────────┘  └─┘
typ                                               └─────────┘  └─┘  └┘
doc                                                     └─────────┘
314  lift'.is_ring_hom _ _ _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
315  
316  @[simp] lemma map_of (hf : ∀ s ∈ S, f s ∈ T) (a : α) :
id                                               
src                                          
typ                                              
doc    └──┘
317    map f hf (of a) = of (f a) := lift'_of _ _ _ _
id     └─┘  └┘  └┘    └┘        └──────┘
src    └─┘       └┘     └┘          └──────┘
typ    └─┘  └┘  └┘    └┘        └──────┘
doc              └┘      └┘
318  
319  @[simp] lemma map_coe (hf : ∀ s ∈ S, f s ∈ T) (a : α) :
id                                                
src                                           
typ                                               
doc    └──┘
320    map f hf a = (f a) := lift'_of _ _ _ _
id     └─┘  └┘          └──────┘
src    └─┘                  └──────┘
typ    └─┘  └┘          └──────┘
321  
322  @[simp] lemma map_comp_of (hf : ∀ s ∈ S, f s ∈ T) :
id                                             
src                                               
typ                                            
doc    └──┘
323    map f hf ∘ of = of ∘ f := funext $ λ a, map_of _ _ _
id     └─┘  └┘  └┘  └┘      └────┘       └────┘
src    └─┘       └┘  └┘       └────┘        └────┘
typ    └─┘  └┘  └┘  └┘      └────┘       └────┘
doc               └┘   └┘
324  
325  @[simp] lemma map_id : map id (λ s (hs : s ∈ S), hs) = id :=
id                          └─┘ └┘                └┘   └┘
src                         └─┘ └┘                        └┘
typ                         └─┘ └┘                └┘   └┘
doc    └──┘
326  localization.funext _ _ $ map_coe _ _
id   └─────────────────┘       └─────┘
src  └─────────────────┘       └─────┘
typ  └─────────────────┘       └─────┘
doc  └─────────────────┘
327  
328  lemma map_comp_map {γ : Type*} [comm_ring γ]  (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
id                                   └───────┘                           └─┘ 
src                                  └───────┘                                 └─┘
typ                                  └───────┘                           └─┘ 
329    [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) :
id      └──────────┘              └─────────┘                   
src     └──────────┘                 └─────────┘                       
typ     └──────────┘              └─────────┘                   
doc     └──────────┘                 └─────────┘
330    map g hg ∘ map f hf = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) :=
id     └─┘  └┘  └─┘  └┘  └─┘                └┘  └┘    └┘   └┘
src    └─┘       └─┘       └─┘
typ    └─┘  └┘  └─┘  └┘  └─┘                └┘  └┘    └┘   └┘
331  localization.funext _ _ $ by simp
id   └─────────────────┘
src  └─────────────────┘          └────
typ  └─────────────────┘          └────
doc  └─────────────────┘          └────
txt                               └────
par                               └────
pid                                   
st                               └─────
332  
src  
typ  
doc  
txt  
par  
pid  
st   
333  lemma map_map {γ : Type*} [comm_ring γ]  (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
id                              └───────┘                           └─┘ 
src                             └───────┘                                 └─┘
typ                             └───────┘                           └─┘ 
334    [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) (x) :
id      └──────────┘              └─────────┘                   
src     └──────────┘                 └─────────┘                       
typ     └──────────┘              └─────────┘                   
doc     └──────────┘                 └─────────┘
335    map g hg (map f hf x) = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) x :=
id     └─┘  └┘  └─┘  └┘    └─┘                └┘  └┘    └┘   └┘   
src    └─┘       └─┘          └─┘
typ    └─┘  └┘  └─┘  └┘    └─┘                └┘  └┘    └┘   └┘   
336  congr_fun (map_comp_map _ _ _ _ _) x
id   └───────┘  └──────────┘            
src  └───────┘  └──────────┘
typ  └───────┘  └──────────┘            
337  
338  def equiv_of_equiv (h₁ : α ≃+* β) (h₂ : h₁ '' S = T) :
id                             └─┘         └┘ └┘   
src                             └─┘             └┘   
typ                            └─┘         └┘ └┘   
339    localization α S ≃+* localization β T :=
id     └──────────┘   └─┘ └──────────┘  
src    └──────────┘     └─┘ └──────────┘
typ    └──────────┘   └─┘ └──────────┘  
doc    └──────────┘         └──────────┘
340  { to_fun := map h₁ $ λ s hs, h₂ ▸ set.mem_image_of_mem _ hs,
id               └─┘ └┘      └┘  └┘  └──────────────────┘   └┘
src              └─┘                  └──────────────────┘
typ              └─┘ └┘      └┘  └┘  └──────────────────┘   └┘
341    inv_fun := map h₁.symm $ λ t ht,
id                └─┘ └┘└───┘      └┘
src               └─┘   └───┘
typ               └─┘ └┘└───┘      └┘
doc                     └───┘
342      by simp [h₁.image_eq_preimage, set.preimage, set.ext_iff, *] at *,
id                                      └──────────┘  └─────────┘
src         └────┘                    └┘└──────────┘└┘└─────────┘└───────┘
typ         └────┘└──────────────────┘└┘└──────────┘└┘└─────────┘└───────┘
doc         └────┘                    └┘└──────────┘└┘           └───────┘
txt         └────┘                    └┘            └┘           └───────┘
par         └────┘                    └┘            └┘           └───────┘
pid                                 └┘            └┘           └──┘└──┘
st         └─────────────────────────────────────────────────────────────┘
343    left_inv := λ _, by simp only [map_map, h₁.symm_apply_apply]; erw map_id; refl,
id                                   └─────┘                            └────┘
src                        └─────────┘└─────┘└┘                     └──┘└────┘  └──┘
typ                       └─────────┘└─────┘└┘└─────────────────┘  └──┘└────┘  └──┘
doc                        └─────────┘       └┘                     └──┘        └──┘
txt                        └─────────┘       └┘                     └──┘        └──┘
par                        └─────────┘       └┘                     └──┘        └──┘
pid                            └──┘└┘       └┘                        
st                        └─────────────────────────────────────────────┘└────┘└────┘
344    right_inv := λ _, by simp only [map_map, h₁.apply_symm_apply]; erw map_id; refl,
id                                    └─────┘                            └────┘
src                         └─────────┘└─────┘└┘                     └──┘└────┘  └──┘
typ                        └─────────┘└─────┘└┘└─────────────────┘  └──┘└────┘  └──┘
doc                         └─────────┘       └┘                     └──┘        └──┘
txt                         └─────────┘       └┘                     └──┘        └──┘
par                         └─────────┘       └┘                     └──┘        └──┘
pid                             └──┘└┘       └┘                        
st                         └─────────────────────────────────────────────┘└────┘└────┘
345    map_mul' := λ _ _, is_ring_hom.map_mul _,
id                      └─────────────────┘
src                       └─────────────────┘
typ                     └─────────────────┘
346    map_add' := λ _ _, is_ring_hom.map_add _ }
id                      └─────────────────┘
src                       └─────────────────┘
typ                     └─────────────────┘
347  
348  end
349  
350  section away
351  variables {β : Type v} [comm_ring β] (f : α → β) [is_ring_hom f]
id                           └───────┘                 └─────────┘
src                          └───────┘                 └─────────┘
typ                          └───────┘                 └─────────┘
doc                                                    └─────────┘
352  
353  @[reducible] def away (x : α) := localization α (powers x)
id                                   └──────────┘   └────┘ 
src                                   └──────────┘    └────┘
typ                                  └──────────┘   └────┘ 
doc    └───────┘                      └──────────┘    └────┘
354  
355  @[simp] def away.inv_self (x : α) : away x :=
id                                      └──┘ 
src                                      └──┘
typ                                     └──┘ 
doc    └──┘
356  mk 1 ⟨x, 1, pow_one x⟩
id   └┘         └─────┘ 
src  └┘          └─────┘
typ  └┘         └─────┘ 
357  
358  @[elab_with_expected_type]
doc    └─────────────────────┘
359  noncomputable def away.lift {x : α} (hfx : is_unit (f x)) : away x → β :=
id                                             └─────┘        └──┘    
src                                             └─────┘          └──┘
typ                                            └─────┘        └──┘    
doc                                             └─────┘
360  localization.lift' f (λ s, classical.some hfx ^ classical.some s.2) $ λ s,
id   └────────────────┘       └────────────┘ └─┘  └────────────┘        
src  └────────────────┘         └────────────┘      └────────────┘  
typ  └────────────────┘       └────────────┘ └─┘  └────────────┘        
361  by rw [units.coe_pow, ← classical.some_spec hfx,
id          └───────────┘    └─────────────────┘ └─┘
src     └──┘└───────────┘└──┘└─────────────────┘   └─
typ     └──┘└───────────┘└──┘└─────────────────┘└─┘└─
doc     └──┘             └──┘                      └─
txt     └──┘             └──┘                      └─
par     └──┘             └──┘                      └─
pid       └┘             └──┘                      └─
st     └────────────────┘└─────────────────────────┘└─
362         ← is_semiring_hom.map_pow f, classical.some_spec s.2]; refl
id            └─────────────────────┘   └─────────────────┘ 
src  ────────┘└─────────────────────┘ └┘└─────────────────┘ └─┘  └────
typ  ────────┘└─────────────────────┘└┘└─────────────────┘└─┘  └────
doc  ────────┘                        └┘                    └─┘  └────
txt  ────────┘                        └┘                    └─┘  └────
par  ────────┘                        └┘                    └─┘  └────
pid  ────────┘                        └┘                    └─┘      
st   ─────────────────────────────────┘└─────────────────────┘└─┘└──────
363  
src  
typ  
doc  
txt  
par  
pid  
st   
364  instance away.lift.is_ring_hom {x : α} (hfx : is_unit (f x)) :
id                                                └─────┘   
src                                                └─────┘
typ                                               └─────┘   
doc                                                └─────┘
365    is_ring_hom (localization.away.lift f hfx) :=
id     └─────────┘  └────────────────────┘  └─┘
src    └─────────┘  └────────────────────┘
typ    └─────────┘  └────────────────────┘  └─┘
doc    └─────────┘
366  lift'.is_ring_hom _ _ _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
367  
368  @[simp] lemma away.lift_of {x : α} (hfx : is_unit (f x)) (a : α) :
id                                            └─────┘           
src                                            └─────┘
typ                                           └─────┘           
doc    └──┘                                    └─────┘
369    away.lift f hfx (of a) = f a := lift'_of _ _ _ _
id     └───────┘  └─┘  └┘         └──────┘
src    └───────┘        └┘            └──────┘
typ    └───────┘  └─┘  └┘         └──────┘
doc                     └┘
370  
371  @[simp] lemma away.lift_coe {x : α} (hfx : is_unit (f x)) (a : α) :
id                                             └─────┘           
src                                             └─────┘
typ                                            └─────┘           
doc    └──┘                                     └─────┘
372    away.lift f hfx a = f a := lift'_of _ _ _ _
id     └───────┘  └─┘        └──────┘
src    └───────┘                 └──────┘
typ    └───────┘  └─┘        └──────┘
373  
374  @[simp] lemma away.lift_comp_of {x : α} (hfx : is_unit (f x)) :
id                                                 └─────┘   
src                                                 └─────┘
typ                                                └─────┘   
doc    └──┘                                         └─────┘
375    away.lift f hfx ∘ of = f := lift'_comp_of _ _ _
id     └───────┘  └─┘  └┘      └───────────┘
src    └───────┘        └┘       └───────────┘
typ    └───────┘  └─┘  └┘      └───────────┘
doc                      └┘
376  
377  noncomputable def away_to_away_right (x y : α) : away x → away (x * y) :=
id                                                   └──┘    └──┘    
src                                                   └──┘     └──┘    
typ                                                  └──┘    └──┘    
378  localization.away.lift coe $
id   └────────────────────┘ └─┘
src  └────────────────────┘ └─┘
typ  └────────────────────┘ └─┘
379  is_unit_of_mul_one x (y * away.inv_self (x * y)) $
id   └────────────────┘     └───────────┘    
src  └────────────────┘       └───────────┘    
typ  └────────────────┘     └───────────┘    
380  by rw [away.inv_self, coe_mul_mk, coe_mul_mk, mul_one, mk_self]
id          └───────────┘  └────────┘  └────────┘  └─────┘  └─────┘
src     └──┘└───────────┘└┘└────────┘└┘└────────┘└┘└─────┘└┘└─────┘└─
typ     └──┘└───────────┘└┘└────────┘└┘└────────┘└┘└─────┘└┘└─────┘└─
doc     └──┘             └┘          └┘          └┘       └┘       └─
txt     └──┘             └┘          └┘          └┘       └┘       └─
par     └──┘             └┘          └┘          └┘       └┘       └─
pid       └┘             └┘          └┘          └┘       └┘       
st     └────────────────┘└──────────┘└──────────┘└───────┘└───────┘
381  
src  
typ  
doc  
txt  
par  
pid  
st   
382  instance away_to_away_right.is_ring_hom (x y : α) :
id                                                  
typ                                                 
383    is_ring_hom (away_to_away_right x y) :=
id     └─────────┘  └────────────────┘  
src    └─────────┘  └────────────────┘
typ    └─────────┘  └────────────────┘  
doc    └─────────┘
384  away.lift.is_ring_hom _ _
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
385  
386  end away
387  
388  section at_prime
389  
390  variables (P : ideal α) [hp : ideal.is_prime P]
id                  └───┘          └────────────┘
src                 └───┘          └────────────┘
typ                 └───┘          └────────────┘
391  include hp
392  
393  instance prime.is_submonoid :
394    is_submonoid (-P : set α) :=
id     └──────────┘     └─┘ 
src    └──────────┘      └─┘
typ    └──────────┘     └─┘ 
doc    └──────────┘
395  { one_mem := P.ne_top_iff_one.1 hp.1,
id                └─────────────┘  └┘
src                └─────────────┘    
typ               └─────────────┘  └┘
396    mul_mem := λ x y hnx hny hxy, or.cases_on (hp.2 hxy) hnx hny }
id                    └─┘ └─┘ └─┘  └─────────┘  └┘  └─┘  └─┘ └─┘
src                                  └─────────┘    
typ                   └─┘ └─┘ └─┘  └─────────┘  └┘  └─┘  └─┘ └─┘
397  
398  @[reducible] def at_prime := localization α (-P)
id                                └──────────┘   
src                               └──────────┘    
typ                               └──────────┘   
doc    └───────┘                  └──────────┘
399  
400  instance at_prime.local_ring : local_ring (at_prime P) :=
id                                  └────────┘  └──────┘ 
src                                 └────────┘  └──────┘
typ                                 └────────┘  └──────┘ 
401  local_of_nonunits_ideal
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
402    (λ hze,
id        └─┘
typ       └─┘
403      let ⟨t, hts, ht⟩ := quotient.exact hze in
id       └─┘    └─┘         └────────────┘ └─┘
src                          └────────────┘
typ      └─┘    └─┘         └────────────┘ └─┘
404      hts $ have htz : t = 0, by simpa using ht,
id                                             └┘
src                                └──────────┘
typ                                └──────────┘└┘
doc                                 └──────────┘
txt                                 └──────────┘
par                                 └──────────┘
pid                                      └────┘
st                                 └─────────────┘
405        suffices (0:α) ∈ P, by rwa htz,
id                                 └─┘
src                              └──┘
typ                            └──┘└─┘
doc                               └──┘
txt                               └──┘
par                               └──┘
pid                                  
st                               └──────┘
406        P.zero_mem)
id         └───────┘
src         └───────┘
typ        └───────┘
407    (begin
st      └─────
408      rintro ⟨⟨r₁, s₁, hs₁⟩⟩ ⟨⟨r₂, s₂, hs₂⟩⟩ hx hy hu,
src      └─────────────────────────────────────────────┘
typ      └─────────────────────────────────────────────┘
doc      └─────────────────────────────────────────────┘
txt      └─────────────────────────────────────────────┘
par      └─────────────────────────────────────────────┘
pid            └───────────────────────────────────────┘
st   ──────────────────────────────────────────────────┘└─
409      rcases is_unit_iff_exists_inv.1 hu with ⟨⟨⟨r₃, s₃, hs₃⟩⟩, hz⟩,
id              └────────────────────┘   └┘
src      └─────┘└────────────────────┘└─┘  └─────────────────────────┘
typ      └─────┘└────────────────────┘└─┘└┘└─────────────────────────┘
doc      └─────┘                      └─┘  └─────────────────────────┘
txt      └─────┘                      └─┘  └─────────────────────────┘
par      └─────┘                      └─┘  └─────────────────────────┘
pid                                  └─┘  └─────────────────────────┘
st   ────────────────────────────────────────────────────────────────┘└─
410      rcases quotient.exact hz with ⟨t, hts, ht⟩,
id              └────────────┘ └┘
src      └─────┘└────────────┘  └────────────────┘
typ      └─────┘└────────────┘└┘└────────────────┘
doc      └─────┘                └────────────────┘
txt      └─────┘                └────────────────┘
par      └─────┘                └────────────────┘
pid                            └────────────────┘
st   ─────────────────────────────────────────────┘└─
411      simp at ht,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid          └───┘
st   ─────────────┘└─
412      have : ∀ {r s hs}, (⟦⟨r, s, hs⟩⟧ : at_prime P) ∈ nonunits (at_prime P) → r ∈ P,
id                                                     └──────┘  └──────┘          
src      └─────┘ └───────┘    └┘ └┘  └─┘         └┘└──────┘ └──────┘ └┘   
typ      └─────┘ └───────┘    └┘ └┘  └─┘         └┘└──────┘ └──────┘ └┘   
doc      └─────┘ └───────┘     └┘ └┘   └─┘         └┘                   └┘   
txt      └─────┘ └───────┘     └┘ └┘   └─┘         └┘                   └┘   
par      └─────┘ └───────┘     └┘ └┘   └─┘         └┘                   └┘   
pid      └───┘└┘ └───────┘     └┘ └┘   └─┘         └┘                   └┘   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
413      { haveI := classical.dec,
id                  └───────────┘
src        └───────┘└───────────┘
typ        └───────┘└───────────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid             └─┘
st   ─────┘└────────────────────┘└─
414        exact λ r s hs, not_imp_comm.1 (λ nr,
id                         └──────────┘
src        └────┘ └───────┘└──────────┘└─┘  └────
typ        └────┘ └───────┘└──────────┘└─┘  └────
doc        └────┘ └───────┘            └─┘  └────
txt        └────┘ └───────┘            └─┘  └────
par        └────┘ └───────┘            └─┘  └────
pid              └───────┘            └─┘  └────
st   ────────────────────────────────────────────
415          is_unit_iff_exists_inv.2 ⟨⟦⟨s, r, nr⟩⟧,
id           └────────────────────┘
src  ───────┘└────────────────────┘└─┘    └┘ └┘   └─
typ  ───────┘└────────────────────┘└─┘    └┘ └┘   └─
doc  ───────┘                      └─┘    └┘ └┘   └─
txt  ───────┘                      └─┘    └┘ └┘   └─
par  ───────┘                      └─┘    └┘ └┘   └─
pid  ───────┘                      └─┘    └┘ └┘   └─
st   ────────────────────────────────────────────────
416            quotient.sound $ r_of_eq $ by simp [mul_comm]⟩) },
id             └────────────┘   └─────┘            └──────┘
src  ─────────┘└────────────┘ └─────┘   └────┘└──────┘└─┘
typ  ─────────┘└────────────┘ └─────┘   └────┘└──────┘└─┘
doc  ─────────┘                         └────┘        └─┘
txt  ─────────┘                         └────┘        └─┘
par  ─────────┘                         └────┘        └─┘
pid  ─────────┘                         └─────┘        └─┘
st   ──────────────────────────────────────┘└──────────────┘└─┘└┘
417      have hr₃ := (hp.mem_or_mem_of_mul_eq_zero ht).resolve_right hts,
id                    └──────────────────────────┘ └┘                └─┘
src      └──────────┘ └──────────────────────────┘  └──────────────┘
typ      └──────────┘ └──────────────────────────┘└┘└──────────────┘└─┘
doc      └──────────┘                               └──────────────┘
txt      └──────────┘                               └──────────────┘
par      └──────────┘                               └──────────────┘
pid      └──────┘└─┘                               └──────────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
418      have := (ideal.add_mem_iff_left _ _).1 hr₃,
id                └────────────────────┘        └─┘
src      └──────┘ └────────────────────┘└──────┘
typ      └──────┘ └────────────────────┘└──────┘└─┘
doc      └──────┘                       └──────┘
txt      └──────┘                       └──────┘
par      └──────┘                       └──────┘
pid      └───┘└─┘                       └──────┘
st   ─────────────────────────────────────────────┘└─
419      { exact not_or (mt hp.mem_or_mem (not_or hs₁ hs₂)) hs₃ (hp.mem_or_mem this) },
id                       └┘                └────┘ └─┘ └─┘   └─┘  └───────────┘ └──┘
src        └────┘       └┘              └────┘      └─┘    └───────────┘    └┘
typ        └────┘       └┘              └────┘└─┘└─┘└─┘└─┘ └───────────┘└──┘└┘
doc        └────┘                                   └─┘                     └┘
txt        └────┘                                   └─┘                     └┘
par        └────┘                                   └─┘                     └┘
pid                                                └─┘                     
st   ─────┘└────────────────────────────────────────────────────────────────────────┘└┘
420      { exact P.neg_mem (P.mul_mem_right
id               └───────┘  └─────────────┘
src        └────┘└───────┘ └─────────────┘
typ        └────┘└───────┘ └─────────────┘
doc        └────┘                         
txt        └────┘                         
par        └────┘                         
pid                                      
st   ───────────────────────────────────────
421          (P.add_mem (P.mul_mem_left (this hy)) (P.mul_mem_left (this hx)))) }
id            └───────┘                       └┘    └────────────┘  └──┘ └┘
src  ───────┘ └───────┘                      └─┘ └────────────┘       └───┘
typ  ───────┘ └───────┘                    └┘└─┘ └────────────┘ └──┘└┘└───┘
doc  ───────┘                                └─┘                      └───┘
txt  ───────┘                                └─┘                      └───┘
par  ───────┘                                └─┘                      └───┘
pid  ───────┘                                └─┘                      └──┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
422    end)
st   ────┘
423  
424  end at_prime
425  
426  variable (α)
427  
428  def non_zero_divisors : set α := {x | ∀ z, z * x = 0 → z = 0}
id                           └─┘                     
src                          └─┘                           
typ                          └─┘                     
429  
430  instance non_zero_divisors.is_submonoid : is_submonoid (non_zero_divisors α) :=
id                                             └──────────┘  └───────────────┘ 
src                                            └──────────┘  └───────────────┘
typ                                            └──────────┘  └───────────────┘ 
doc                                            └──────────┘
431  { one_mem := λ z hz, by rwa mul_one at hz,
id                   └┘         └─────┘
src                          └──┘└─────┘└────┘
typ                  └┘     └──┘└─────┘└────┘
doc                          └──┘       └────┘
txt                          └──┘       └────┘
par                          └──┘       └────┘
pid                                    └────┘
st                          └────────────────┘
432    mul_mem := λ x₁ x₂ hx₁ hx₂ z hz,
id                  └┘ └┘ └─┘ └─┘  └┘
typ                 └┘ └┘ └─┘ └─┘  └┘
433      have z * x₁ * x₂ = 0, by rwa mul_assoc,
id              └┘  └┘            └───────┘
src                            └──┘└───────┘
typ             └┘  └┘        └──┘└───────┘
doc                               └──┘
txt                               └──┘
par                               └──┘
pid                                  
st                               └────────────┘
434      hx₁ z $ hx₂ (z * x₁) this }
id       └─┘    └─┘    └┘  └──┘
src                     
typ      └─┘    └─┘    └┘  └──┘
435  
436  @[simp] lemma non_zero_divisors_one_val : (1 : non_zero_divisors α).val = 1 := rfl
id                                                  └───────────────┘  └─┘        └─┘
src                                                 └───────────────┘   └─┘        └─┘
typ                                                 └───────────────┘  └─┘        └─┘
doc    └──┘
437  
438  /-- The field of fractions of an integral domain.-/
439  @[reducible] def fraction_ring := localization α (non_zero_divisors α)
id                                     └──────────┘   └───────────────┘ 
src                                    └──────────┘    └───────────────┘
typ                                    └──────────┘   └───────────────┘ 
doc    └───────┘                       └──────────┘
440  
441  namespace fraction_ring
442  open function
443  variables {β : Type u} [integral_domain β] [decidable_eq β]
id                          └─────────────┘     └──────────┘
src                          └─────────────┘     └──────────┘
typ                         └─────────────┘     └──────────┘
444  
445  lemma eq_zero_of_ne_zero_of_mul_eq_zero {x y : β} :
id                                                  
typ                                                 
446    x ≠ 0 → y * x = 0 → y = 0 :=
id                    
src                       
typ                   
447  λ hnx hxy, or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
id     └─┘ └─┘  └──────────────┘  └───────────────────────────────┘ └─┘  └─┘
src             └──────────────┘  └───────────────────────────────┘
typ    └─┘ └─┘  └──────────────┘  └───────────────────────────────┘ └─┘  └─┘
448  
449  lemma mem_non_zero_divisors_iff_ne_zero {x : β} :
id                                                
typ                                               
450    x ∈ non_zero_divisors β ↔ x ≠ 0 :=
id       └───────────────┘    
src       └───────────────┘      
typ      └───────────────┘    
451  ⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
id      └┘ └┘  └─────────┘  └┘            └┘  └─────┘  └──┘
src            └─────────┘            └──┘  └┘└─────┘ └──┘
typ     └┘ └┘  └─────────┘  └┘        └──┘└┘└┘└─────┘ └──┘
doc                                   └──┘  └┘       
txt                                   └──┘  └┘       
par                                   └──┘  └┘       
pid                                     └┘  └┘       
st                                   └─────┘└───────┘
452   λ hnx z, eq_zero_of_ne_zero_of_mul_eq_zero hnx⟩
id      └─┘   └───────────────────────────────┘ └─┘
src            └───────────────────────────────┘
typ     └─┘   └───────────────────────────────┘ └─┘
453  
454  variable (β)
455  
456  def inv_aux (x : β × (non_zero_divisors β)) : fraction_ring β :=
id                       └───────────────┘      └───────────┘ 
src                       └───────────────┘       └───────────┘
typ                      └───────────────┘      └───────────┘ 
doc                                                └───────────┘
457  if h : x.1 = 0 then 0 else ⟦⟨x.2, x.1, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧
id   └┘                             └───────────────────────────────┘└──┘  
src  └┘                                └───────────────────────────────┘└──┘   
typ  └┘                             └───────────────────────────────┘└──┘  
458  
459  instance : has_inv (fraction_ring β) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc                      └───────────┘
460  ⟨quotient.lift (inv_aux β) $
id    └───────────┘  └─────┘ 
src   └───────────┘  └─────┘
typ   └───────────┘  └─────┘ 
461    λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨t, hts, ht⟩,
id                                 
typ                                
462    begin
st     └─────
463      have hrs : s₁ * r₂ = 0 + s₂ * r₁,
id                  └┘  └┘     └┘   └┘
src      └─────────┘    └─┘   
typ      └─────────┘└┘└┘└─┘└┘ └┘
doc      └─────────┘      └─┘    
txt      └─────────┘      └─┘    
par      └─────────┘      └─┘    
pid      └──────┘└─┘      └─┘    
st   ───────────────────────────────────┘└─
464        from sub_eq_iff_eq_add.1 (hts _ ht),
id              └───────────────┘    └─┘   └┘
src        └───┘└───────────────┘└─┘    └─┘  
typ        └───┘└───────────────┘└─┘ └─┘└─┘└┘
doc        └───┘                 └─┘    └─┘  
txt        └───┘                 └─┘    └─┘  
par        └───┘                 └─┘    └─┘  
pid        └───┘                 └─┘    └─┘  
st   ────────────────────────────────────────┘└─
465      by_cases hr₁ : r₁ = 0;
id                      └┘
src      └───────┘   └─┘   └┘
typ      └───────┘   └─┘└┘ └┘
doc      └───────┘   └─┘   └┘
txt      └───────┘   └─┘   └┘
par      └───────┘   └─┘   └┘
pid                 └─┘   
st   ───────────────────────────
466      by_cases hr₂ : r₂ = 0;
id                      └┘
src      └───────┘   └─┘   └┘
typ      └───────┘   └─┘└┘ └┘
doc      └───────┘   └─┘   └┘
txt      └───────┘   └─┘   └┘
par      └───────┘   └─┘   └┘
pid                 └─┘   
st   ───────────────────────────
467      simp [hr₁, hr₂] at hrs;
id             └─┘  └─┘
src      └────┘   └┘   └──────┘
typ      └────┘└─┘└┘└─┘└──────┘
doc      └────┘   └┘   └──────┘
txt      └────┘   └┘   └──────┘
par      └────┘   └┘   └──────┘
pid             └┘   └────┘
st   ────────────────────────────
468      simp only [inv_aux, hr₁, hr₂, dif_pos, dif_neg, not_false_iff, subtype.coe_mk, quotient.eq],
id                  └─────┘  └─┘  └─┘  └─────┘  └─────┘  └───────────┘  └────────────┘  └─────────┘
src      └─────────┘└─────┘└┘   └┘   └┘└─────┘└┘└─────┘└┘└───────────┘└┘└────────────┘└┘└─────────┘
typ      └─────────┘└─────┘└┘└─┘└┘└─┘└┘└─────┘└┘└─────┘└┘└───────────┘└┘└────────────┘└┘└─────────┘
doc      └─────────┘       └┘   └┘   └┘       └┘       └┘             └┘              └┘           
txt      └─────────┘       └┘   └┘   └┘       └┘       └┘             └┘              └┘           
par      └─────────┘       └┘   └┘   └┘       └┘       └┘             └┘              └┘           
pid          └──┘└┘       └┘   └┘   └┘       └┘       └┘             └┘              └┘           
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
469      { exfalso,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
st   ─────┘└─────┘└─
470        exact mem_non_zero_divisors_iff_ne_zero.mp hs₁ hrs },
id               └──────────────────────────────────┘ └─┘ └─┘
src        └────┘└──────────────────────────────────┘      
typ        └────┘└──────────────────────────────────┘└─┘└─┘
doc        └────┘                                          
txt        └────┘                                          
par        └────┘                                          
pid                                                       
st   ────────────────────────────────────────────────────────┘└┘
471      { exfalso,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
st   ─────┘└─────┘└─
472        exact mem_non_zero_divisors_iff_ne_zero.mp hs₂ hrs },
id               └──────────────────────────────────┘ └─┘ └─┘
src        └────┘└──────────────────────────────────┘      
typ        └────┘└──────────────────────────────────┘└─┘└─┘
doc        └────┘                                          
txt        └────┘                                          
par        └────┘                                          
pid                                                       
st   ────────────────────────────────────────────────────────┘└┘
473      { apply r_of_eq,
id               └─────┘
src        └────┘└─────┘
typ        └────┘└─────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────┘
474        simpa [mul_comm] using hrs.symm }
st                                         └─
475    end⟩
st   ────┘
476  
477  lemma mk_inv {r s} :
478    (mk r s : fraction_ring β)⁻¹ =
id      └┘     └───────────┘  └┘ 
src     └┘       └───────────┘   └┘ 
typ     └┘     └───────────┘  └┘ 
doc              └───────────┘
479    if h : r = 0 then 0 else ⟦⟨s, r, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧ := rfl
id     └┘                          └───────────────────────────────┘└──┘      └─┘
src    └┘                             └───────────────────────────────┘└──┘       └─┘
typ    └┘                          └───────────────────────────────┘└──┘      └─┘
480  
481  lemma mk_inv' :
482    ∀ (x : β × (non_zero_divisors β)), (⟦x⟧⁻¹ : fraction_ring β) =
id              └───────────────┘      └┘   └───────────┘   
src               └───────────────┘        └┘   └───────────┘    
typ             └───────────────┘      └┘   └───────────┘   
doc                                                └───────────┘
483    if h : x.1 = 0 then 0 else ⟦⟨x.2.val, x.1, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧
id     └┘                        └─┘      └───────────────────────────────┘└──┘  
src    └┘                          └─┘       └───────────────────────────────┘└──┘   
typ    └┘                        └─┘      └───────────────────────────────┘└──┘  
484  | ⟨r,s,hs⟩ := rfl
id                 └─┘
src                └─┘
typ                └─┘
485  
486  instance : decidable_eq (fraction_ring β) :=
id              └──────────┘  └───────────┘ 
src             └──────────┘  └───────────┘
typ             └──────────┘  └───────────┘ 
doc                           └───────────┘
487  @quotient.decidable_eq (β × non_zero_divisors β) (localization.setoid β (non_zero_divisors β)) $
id    └───────────────────┘    └───────────────┘    └─────────────────┘   └───────────────┘ 
src   └───────────────────┘     └───────────────┘     └─────────────────┘    └───────────────┘
typ   └───────────────────┘    └───────────────┘    └─────────────────┘   └───────────────┘ 
488  λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩, show decidable (∃ t ∈ non_zero_divisors β, (s₁ * r₂ - s₂ * r₁) * t = 0),
id     └┘  └┘       └┘  └┘             └───────┘      └───────────────┘                     
src                                      └───────┘       └───────────────┘                       
typ    └┘  └┘       └┘  └┘             └───────┘      └───────────────┘                     
489  from decidable_of_iff (s₁ * r₂ - s₂ * r₁ = 0)
id        └──────────────┘                 
src       └──────────────┘                 
typ       └──────────────┘                 
490  ⟨λ H, ⟨1, λ y, (mul_one y).symm ▸ id, H.symm ▸ zero_mul _⟩,
id                 └─────┘  └──┘   └┘  └───┘  └──────┘
src                  └─────┘   └──┘   └┘   └───┘  └──────┘
typ                └─────┘  └──┘   └┘  └───┘  └──────┘
491  λ ⟨t, ht1, ht2⟩, or.resolve_right (mul_eq_zero.1 ht2) $ λ ht,
id       └─┘  └─┘   └──────────────┘  └─────────┘           └┘
src                   └──────────────┘  └─────────┘
typ      └─┘  └─┘   └──────────────┘  └─────────┘           └┘
doc                                     └─────────┘
492    one_ne_zero (ht1 1 ((one_mul t).symm ▸ ht))⟩
id     └─────────┘          └─────┘   └──┘   └┘
src    └─────────┘          └─────┘   └──┘  
typ    └─────────┘          └─────┘   └──┘   └┘
493  
494  instance : discrete_field (fraction_ring β) :=
id              └────────────┘  └───────────┘ 
src             └────────────┘  └───────────┘
typ             └────────────┘  └───────────┘ 
doc                             └───────────┘
495  by refine
src     └─────┘
typ     └─────┘
doc     └─────┘
txt     └─────┘
par     └─────┘
pid           
st     └───────
496  { inv            := has_inv.inv,
id                       └─────────┘
src   └─────────────────┘└─────────┘└─
typ   └─────────────────┘└─────────┘└─
doc   └─────────────────┘           └─
txt   └─────────────────┘           └─
par   └─────────────────┘           └─
pid   └─────────────────┘           └─
st   ─────────────────────────────────
497    zero_ne_one    := λ hzo,
src  ───────────────────┘ └─────
typ  ───────────────────┘ └─────
doc  ───────────────────┘ └─────
txt  ───────────────────┘ └─────
par  ───────────────────┘ └─────
pid  ───────────────────┘ └─────
st   ───────────────────────────
498      let ⟨t, hts, ht⟩ := quotient.exact hzo in
id                           └────────────┘
src  ───┘     └┘   └┘  └───┘└────────────┘   └───
typ  ───┘     └┘   └┘  └───┘└────────────┘   └───
doc  ───┘     └┘   └┘  └───┘                 └───
txt  ───┘     └┘   └┘  └───┘                 └───
par  ───┘     └┘   └┘  └───┘                 └───
pid  ───┘     └┘   └┘  └───┘                 └───
st   ──────────────────────────────────────────────
499      zero_ne_one (by simpa using hts _ ht : 0 = 1),
id       └─────────┘                 └─┘         
src  ───┘└─────────┘   └──────────┘   └─┘  └──┘└────
typ  ───┘└─────────┘   └──────────┘└─┘└─┘ └──┘└────
doc  ───┘              └──────────┘   └─┘  └──┘ └────
txt  ───┘              └──────────┘   └─┘  └──┘ └────
par  ───┘              └──────────┘   └─┘  └──┘ └────
pid  ───┘              └───────────┘   └─┘  └───┘ └────
st   ──────────────────┘└──────────────────┘ └─────────
500    mul_inv_cancel := quotient.ind _,
src  ───────────────────┘            └───
typ  ───────────────────┘            └───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
st   ────────────────────────────────────
501    inv_mul_cancel := quotient.ind _,
id                       └──────────┘
src  ───────────────────┘└──────────┘└───
typ  ───────────────────┘└──────────┘└───
doc  ───────────────────┘            └───
txt  ───────────────────┘            └───
par  ───────────────────┘            └───
pid  ───────────────────┘            └───
st   ────────────────────────────────────
502    has_decidable_eq := fraction_ring.decidable_eq β,
id                         └────────────────────────┘ 
src  ─────────────────────┘└────────────────────────┘ └─
typ  ─────────────────────┘└────────────────────────┘└─
doc  ─────────────────────┘                           └─
txt  ─────────────────────┘                           └─
par  ─────────────────────┘                           └─
pid  ─────────────────────┘                           └─
st   ────────────────────────────────────────────────────
503    inv_zero := dif_pos rfl,
id                 └─────┘ └─┘
src  ─────────────┘└─────┘└─┘└─
typ  ─────────────┘└─────┘└─┘└─
doc  ─────────────┘          └─
txt  ─────────────┘          └─
par  ─────────────┘          └─
pid  ─────────────┘          └─
st   ───────────────────────────
504    .. localization.comm_ring };
id        └────────────────────┘
src  ────┘└────────────────────┘└┘
typ  ────┘└────────────────────┘└┘
doc  ────┘                      └┘
txt  ────┘                      └┘
par  ────┘                      └┘
pid  ────┘                      └┘
st   ──────────────────────────────┘
505  { intros x hnx,
506    rcases x with ⟨x, z, hz⟩,
507    have : x ≠ 0,
508      from assume hx, hnx (quotient.sound $ r_of_eq $ by simp [hx]),
509    simp only [has_inv.inv, inv_aux, quotient.lift_beta, dif_neg this],
510    exact (quotient.sound $ r_of_eq $ by simp [mul_comm]) }
st                                                           └┘
511  
512  @[simp] lemma mk_eq_div {r s} : (mk r s : fraction_ring β) = (r / s : fraction_ring β) :=
id                                    └┘     └───────────┘          └───────────┘ 
src                                   └┘       └───────────┘             └───────────┘
typ                                   └┘     └───────────┘          └───────────┘ 
doc    └──┘                                    └───────────┘               └───────────┘
513  show _ = _ * dite (s.1 = 0) _ _, by rw [dif_neg (mem_non_zero_divisors_iff_ne_zero.mp s.2)];
id               └──┘    
src              └──┘     
typ              └──┘    
514  exact localization.mk_eq_mul_mk_one _ _
515  
516  variables {β}
517  
518  @[simp] lemma mk_eq_div' (x : β × (non_zero_divisors β)) :
id                                    └───────────────┘ 
src                                    └───────────────┘
typ                                   └───────────────┘ 
doc    └──┘
519    (⟦x⟧ : fraction_ring β) = ((x.1) / ((x.2).val) : fraction_ring β) :=
id         └───────────┘              └─┘     └───────────┘ 
src         └───────────┘                 └─┘     └───────────┘
typ        └───────────┘              └─┘     └───────────┘ 
doc           └───────────┘                             └───────────┘
520  by erw ← mk_eq_div; cases x; refl
id            └───────┘        
src     └────┘└───────┘  └────┘   └────
typ     └────┘└───────┘  └────┘  └────
doc     └────┘           └────┘   └────
txt     └────┘           └────┘   └────
par     └────┘           └────┘   └────
pid        └─┘                       
st     └───────────────────────────────
521  
src  
typ  
doc  
txt  
par  
pid  
st   
522  lemma eq_zero_of (x : β) (h : (of x : fraction_ring β) = 0) : x = 0 :=
id                                 └┘    └───────────┘          
src                                 └┘     └───────────┘            
typ                                └┘    └───────────┘          
doc                                 └┘     └───────────┘
523  begin
st   └─────
524    rcases quotient.exact h with ⟨t, ht, ht'⟩,
id            └────────────┘ 
src    └─────┘└────────────┘ └────────────────┘
typ    └─────┘└────────────┘└────────────────┘
doc    └─────┘               └────────────────┘
txt    └─────┘               └────────────────┘
par    └─────┘               └────────────────┘
pid                         └────────────────┘
st   ──────────────────────────────────────────┘
525    simpa [mem_non_zero_divisors_iff_ne_zero.mp ht] using ht'
526  end
st   └─┘
527  
528  lemma of.injective : function.injective (of : β → fraction_ring β) :=
id                        └────────────────┘  └┘      └───────────┘ 
src                       └────────────────┘  └┘       └───────────┘
typ                       └────────────────┘  └┘      └───────────┘ 
doc                                           └┘       └───────────┘
529  (is_add_group_hom.injective_iff _).mpr eq_zero_of
id    └────────────────────────────┘   └─┘  └────────┘
src   └────────────────────────────┘   └─┘  └────────┘
typ   └────────────────────────────┘   └─┘  └────────┘
530  
531  section map
532  open function is_ring_hom
533  variables {A : Type u} [integral_domain A] [decidable_eq A]
id                           └─────────────┘     └──────────┘
src                          └─────────────┘     └──────────┘
typ                          └─────────────┘     └──────────┘
534  variables {B : Type v} [integral_domain B] [decidable_eq B]
id                           └─────────────┘     └──────────┘
src                          └─────────────┘     └──────────┘
typ                          └─────────────┘     └──────────┘
535  variables (f : A → B) [is_ring_hom f]
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
doc                         └─────────┘
536  
537  def map (hf : injective f) : fraction_ring A → fraction_ring B :=
id                 └───────┘     └───────────┘    └───────────┘ 
src                └───────┘      └───────────┘     └───────────┘
typ                └───────┘     └───────────┘    └───────────┘ 
doc                               └───────────┘     └───────────┘
538  localization.map f $ λ s h,
id   └──────────────┘       
src  └──────────────┘
typ  └──────────────┘       
539    by rw [mem_non_zero_divisors_iff_ne_zero, ← map_zero f, ne.def, hf.eq_iff];
id            └───────────────────────────────┘    └──────┘   └────┘
src       └──┘└───────────────────────────────┘└──┘└──────┘ └┘└────┘└┘         
typ       └──┘└───────────────────────────────┘└──┘└──────┘└┘└────┘└┘└───────┘
doc       └──┘                                 └──┘└──────┘ └┘      └┘         
txt       └──┘                                 └──┘         └┘      └┘         
par       └──┘                                 └──┘         └┘      └┘         
pid         └┘                                 └──┘         └┘      └┘         
st       └────────────────────────────────────┘└────────────┘└──────┘└─────────┘└─
540      exact mem_non_zero_divisors_iff_ne_zero.1 h
id             └───────────────────────────────┘   
src      └────┘└───────────────────────────────┘└─┘ 
typ      └────┘└───────────────────────────────┘└─┘
doc      └────┘                                 └─┘ 
txt      └────┘                                 └─┘ 
par      └────┘                                 └─┘ 
pid                                            └─┘ 
st   ────────────────────────────────────────────────
541  
src  
typ  
doc  
txt  
par  
pid  
st   
542  @[simp] lemma map_of (hf : injective f) (a : A) : map f hf (of a) = of (f a) :=
id                              └───────┘            └─┘  └┘  └┘    └┘   
src                             └───────┘              └─┘       └┘     └┘
typ                             └───────┘            └─┘  └┘  └┘    └┘   
doc    └──┘                                                      └┘      └┘
543  localization.map_of _ _ _
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
544  
545  @[simp] lemma map_coe (hf : injective f) (a : A) : map f hf a = f a :=
id                               └───────┘            └─┘  └┘    
src                              └───────┘              └─┘        
typ                              └───────┘            └─┘  └┘    
doc    └──┘
546  localization.map_coe _ _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
547  
548  @[simp] lemma map_comp_of (hf : injective f) :
id                                   └───────┘ 
src                                  └───────┘
typ                                  └───────┘ 
doc    └──┘
549    map f hf ∘ (of : A → fraction_ring A) = (of : B → fraction_ring B) ∘ f :=
id     └─┘  └┘   └┘      └───────────┘     └┘      └───────────┘    
src    └─┘        └┘       └───────────┘      └┘       └───────────┘    
typ    └─┘  └┘   └┘      └───────────┘     └┘      └───────────┘    
doc                └┘       └───────────┘       └┘       └───────────┘
550  localization.map_comp_of _ _
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
551  
552  instance map.is_ring_hom (hf : injective f) : is_ring_hom (map f hf) :=
id                                  └───────┘     └─────────┘  └─┘  └┘
src                                 └───────┘      └─────────┘  └─┘
typ                                 └───────┘     └─────────┘  └─┘  └┘
doc                                                └─────────┘
553  localization.map.is_ring_hom _ _
id   └──────────────────────────┘
src  └──────────────────────────┘
typ  └──────────────────────────┘
554  
555  def equiv_of_equiv (h : A ≃+* B) : fraction_ring A ≃+* fraction_ring B :=
id                            └─┘     └───────────┘  └─┘ └───────────┘ 
src                            └─┘      └───────────┘   └─┘ └───────────┘
typ                           └─┘     └───────────┘  └─┘ └───────────┘ 
doc                                     └───────────┘       └───────────┘
556  localization.equiv_of_equiv h
id   └─────────────────────────┘ 
src  └─────────────────────────┘
typ  └─────────────────────────┘ 
557  begin
st   └─────
558    ext b,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
559    rw [h.image_eq_preimage, set.preimage, set.mem_set_of_eq,
id                              └──────────┘  └───────────────┘
src    └──┘                   └┘└──────────┘└┘└───────────────┘└─
typ    └──┘└─────────────────┘└┘└──────────┘└┘└───────────────┘└─
doc    └──┘                   └┘└──────────┘└┘                 └─
txt    └──┘                   └┘            └┘                 └─
par    └──┘                   └┘            └┘                 └─
pid      └┘                   └┘            └┘                 └─
st   ────────────────────────┘└────────────┘└─────────────────┘└─
560      mem_non_zero_divisors_iff_ne_zero, mem_non_zero_divisors_iff_ne_zero, ne.def],
id       └───────────────────────────────┘  └───────────────────────────────┘
src  ───┘└───────────────────────────────┘ └───────────────────────────────┘
typ  ───┘└───────────────────────────────┘ └───────────────────────────────┘
doc  ───┘                                 
txt  ───┘                                 
par  ───┘                                 
pid  ───┘                                 
st   ────────────────────────────────────┘ └───────────────────────────────┘
561    exact h.symm.map_ne_zero_iff
id           └────────────────────┘
src          └────────────────────┘
typ          └────────────────────┘
doc          └────────────────────┘
562  end
st   └─┘
563  
564  end map
565  
566  end fraction_ring
567  
568  section ideals
569  
570  theorem map_comap (J : ideal (localization α S)) :
id                          └───┘  └──────────┘  
src                         └───┘  └──────────┘
typ                         └───┘  └──────────┘  
doc                                └──────────┘
571    ideal.map coe (ideal.comap (coe : α → localization α S) J) = J :=
id     └───────┘ └─┘  └─────────┘  └─┘      └──────────┘       
src    └───────┘ └─┘  └─────────┘  └─┘       └──────────┘         
typ    └───────┘ └─┘  └─────────┘  └─┘      └──────────┘       
doc                   └─────────┘            └──────────┘
572  le_antisymm (ideal.map_le_iff_le_comap.2 (le_refl _)) $ λ x,
id   └─────────┘  └───────────────────────┘   └─────┘         
src  └─────────┘  └───────────────────────┘   └─────┘
typ  └─────────┘  └───────────────────────┘   └─────┘         
573  localization.induction_on x $ λ r s hJ, (submodule.mem_coe _).2 $
id   └───────────────────────┘             └───────────────┘   
src  └───────────────────────┘                └───────────────┘   
typ  └───────────────────────┘             └───────────────┘   
574  mul_one r ▸ coe_mul_mk r 1 s ▸ (ideal.mul_mem_right _ $ ideal.mem_map_of_mem $
id   └─────┘   └────────┘       └─────────────────┘     └──────────────────┘
src  └─────┘    └────────┘         └─────────────────┘     └──────────────────┘
typ  └─────┘   └────────┘       └─────────────────┘     └──────────────────┘
575  have _ := @ideal.mul_mem_left (localization α S) _ _ s _ hJ,
id              └────────────────┘  └──────────┘        
src             └────────────────┘  └──────────┘
typ             └────────────────┘  └──────────┘        
doc                                 └──────────┘
576  by rwa [coe_coe, coe_mul_mk, mk_mul_cancel_left] at this)
577  
578  def le_order_embedding :
579    ((≤) : ideal (localization α S) → ideal (localization α S) → Prop) ≼o
id           └───┘  └──────────┘      └───┘  └──────────┘            └┘
src          └───┘  └──────────┘        └───┘  └──────────┘              └┘
typ          └───┘  └──────────┘      └───┘  └──────────┘            └┘
doc                  └──────────┘               └──────────┘              └┘
580    ((≤) : ideal α → ideal α → Prop) :=
id           └───┘    └───┘ 
src          └───┘     └───┘
typ          └───┘    └───┘ 
581  { to_fun := λ J, ideal.comap coe J,
id                   └─────────┘ └─┘ 
src                   └─────────┘ └─┘
typ                  └─────────┘ └─┘ 
doc                   └─────────┘
582    inj := function.injective_of_left_inverse (map_comap α),
id            └────────────────────────────────┘  └───────┘ 
src           └────────────────────────────────┘  └───────┘
typ           └────────────────────────────────┘  └───────┘ 
583    ord := λ J₁ J₂, ⟨ideal.comap_mono, λ hJ,
id              └┘ └┘   └──────────────┘
src                     └──────────────┘
typ             └┘ └┘   └──────────────┘
584      map_comap α J₁ ▸ map_comap α J₂ ▸ ideal.map_mono hJ⟩ }
id                                 
typ                                
585  
586  end ideals
587  
588  end localization